git.iko.soy/Idris-dev
on dee61df help sign in
history ofsrc/Idris/Parser.hs
all commits
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 319582eElaborate lhs of pattern clause properly in implicit argumentsEdwin Brady 29c67e9Pattern matching on strings, big integers and charactersEdwin Brady af66f25Added 'mutual' blocks Effect is to elaborate all types in the block before elaborating definitionsEdwin Brady 895b323Allow forward declaration of data structures To support induction-recursion and mutual data definitions Syntax is as a normal data declaration, but without the 'where' or '=' sectionsEdwin Brady 671d39aFix name clashes between holes and bound variablesEdwin Brady 7438e0fDocument --warnpartial Behaviour fixed so that it doesn't report declared partial functionsEdwin Brady 9affb75Totality checker improvements Now does a better job of checking type class instances for totality, by inlining dictionaries where possible. Added %default total declarations to some libraries where possibleEdwin Brady 5692e48Added "codata" Constructors of coinductive types evaluate arguments lazily. Corecursive functions do not reduce at compile time.Edwin Brady