git.iko.soy/Idris-dev
on ff0fbfa help sign in
history ofsrc/Idris/Parser.hs
all commits
7308d26Remove type class argument restriction in parserEdwin Brady ab498e9Add syntax for language extensions and turn off type providers by defaultDavid Christiansen 161ef3dMerge remote-tracking branch 'upstream/master' into providersDavid Christiansen db5973bAdded rewrite ... in ... construct rewrite prf in v rewrites the goal type using prf. It is equivalent to applying replace, without the need to provide a predicate. It works by applying the rewrite tactic with prf before elaborating v.Edwin Brady 3a80954%dynamic now works from IBC filesDavid Christiansen 04267d6Top-level directive for dynamic linkingDavid Christiansen 0f49abcAdded first steps in type providersDavid Christiansen 6e732f9Added %provide directive to parserDavid Christiansen 0b58ae0Missing case in Idris.ParserMichael Thompson a5ea29fMerge pull request #203 from david-christiansen/haddockEdwin Brady 422521fTweak syntax rules to deal with consecutive non-terminals betterEdwin Brady 22c355aDocumentation comment additionsDavid Christiansen 022d4dfAdded 'implicit' conversions implicit f : a -> b Then, when a function needs a 'b' but has an 'a', f will be called implicitly. This is probably scary and fragile. Use with extreme caution!Edwin Brady 82a4e9bFix for line numbers on type signaturesEdwin Brady 4c5b1bdMerge branch 'master' into bitstringBenjamin Saunders 1eed9c2Merge pull request #181 from raichoo/masterEdwin Brady 37ed162load command should ignore trailing whitespacesraichoo e49ab72Reorder the monad transformers in the Idris monad to allow completionDavid Christiansen 41f3d97Merge branch 'master' of git://github.com/edwinb/Idris-dev into bitstringBenjamin Saunders 1ffdfc0Parse case options as patterns, not expressions Fixes issue #147Edwin Brady b2cf967Allow class constraints in syntax definitionsEdwin Brady 04d6f00A small amount of proof automation, via tactic reflectionEdwin Brady b896224Primitive types for groups of 8, 16, 32, and 64 bits, and basic arithmetic and mutual conversion operations on themBenjamin Saunders 60dbc48Add %instance for explicit access to resolveTC tacticEdwin Brady 8d090c0A couple of small improvements to termination checking * inlining to help out * %assert_total doesn't allow inlining so as not to break totality for functions which rely on the asserted function * bug fix for mutual recursion - build size graphs before doing any totality checkingEdwin Brady 0a70480Merge branch 'type' of https://github.com/raichoo/Idris-dev into raichoo-typeEdwin Brady dd5001fmake TT aware of Set -> Typeraichoo 12f7a82Allow documentation comments for records.startling 7fefa89PSet -> PTyperaichoo cc716d7Make 'Type' the type of types instead of Sets ...after mailing list discussionEdwin Brady 441f51dpossible fixes for missing type signature in data declsraichoo ed85b4eerror messages with possible fixesraichoo f6451efword 8/16 primitive typesraichoo e23c029Allow type annotations on let tacticEdwin Brady 160eeddMerge pull request #101 from chetant/windowsEdwin Brady 51f3340Merge pull request #99 from raichoo/masterEdwin Brady fab5d73Adding support for Windows MingW32chetant b1cdd04Added postulate declarations postulate foo : type -- 'type' must return something of a collapsible type, i.e. a type with at most one instancei determined entirely by the indices, to ensure that it is unused at run-time.Edwin Brady 2250085indent fixity error messageraichoo 5d33da2removed "user error" from error messagesraichoo 809c283Merge pull request #90 from raichoo/parserEdwin Brady bbe9dc1Minor fixes for inlining and integer literalsEdwin Brady 92f3139eof should close all open blocksraichoo 40ce0cabetter fixity error messageraichoo c9e0444show actual ParseError messageraichoo ff56693prevent different fixity declarationsraichoo a777c93Change 'abstract' rule for records Still have access to field names, but not constructor nameEdwin Brady 1ccd94aSyntax for documentation comments and :doc REPL commandEdwin Brady 8464bc4Add field for documentation comments in abstract syntaxEdwin Brady 6d7a6aaChange comment rules Comments cannot begin '{-|' or '--|'. This is now reserved for documentation comments, which will be part of the syntax to support documentation at the REPL.Edwin Brady