git.iko.soy/Idris-dev
on bbaa193 help sign in
history ofsrc/Idris/Parser.hs
all commits
bbaa193Better representation of namesEdwin Brady ae3ad10Apply fromInteger for negative numbersEdwin Brady 925648aAdd %include directiveEdwin Brady 374fc26Add let x = t tacticEdwin Brady 8d83d07Type declarations of the form (x,y,z : A) -> BEdwin Brady e89453fAllow type labels on sigma bindingsEdwin Brady 1c49219Added provisional definitionsEdwin Brady 4931c20Added Integer (but an Epic bug prevents them compiling properly)Edwin Brady e530718Add fromInteger to Nat class; allow type labels on letEdwin Brady f1c7fafAdded tactics construct, and tactic sequencing/choiceEdwin Brady 71c1a0eExtension parsing, now deferring checks name is uniqueEdwin Brady 4a1324cDistinguish term syntax and pattern syntaxEdwin Brady 31d974bMore flexibility with syntax definitionsEdwin Brady 2e02cf6Logging optionsEdwin Brady 5afe678Added log/exp (and lib/link directives)Edwin Brady ffc64e3Add mechanism for simplification and function optionsEdwin Brady 169d8c0Elaborating instance declarationsEdwin Brady f2459a5Added class constraintsEdwin Brady 13d08bdElaborating class declarationsEdwin Brady 33710abParsing class and instance (but no elaboration yet)Edwin Brady 5528447Not really mini any more...Edwin Brady 229a99cBetter elaboration order; also changed instance argument syntax slightlyEdwin Brady be3a53aType class instance resolution, and some Num overloadingEdwin Brady 22546bc:r and :e at the REPL.Edwin Brady 1b1a055Improved where; implicit arguments now expanded during elaborationEdwin Brady 188dda5Tinkering with tactics and deferred definitionsEdwin Brady 58bd7c4Added rewrite tacticEdwin Brady 10b88aeAdded refine, focus, undoEdwin Brady ebcb29bAdded proof script traces for pasting into programEdwin Brady 551548cBeginning theorem prover interfaceEdwin Brady 3bdfa26Added [static] annotations (which do nothing yet) and state to evaluatorEdwin Brady b85965eparser tinkeringEdwin Brady 1155e79Laziness annotationsEdwin Brady 95a558bAdded = and reflEdwin Brady 5fbca2aFix with so that clauses are checked for matches against top level defnEdwin Brady 39b934cSugar for dependent pairsEdwin Brady 5e92c70When collecting implicit args in wheres, ignore names bound in above scopeEdwin Brady bf368abFirst attempt at with ruleEdwin Brady cc4eb28let bindings; fixed bug with simple lambda appEdwin Brady 796fa25BannerEdwin Brady 5f7eed8Propagate line numbers through applications and variablesEdwin Brady ec87a69Some effort at reporting line numbers of errors (top level of decl only)Edwin Brady 180e979Added builtins.idr and fixed a bug or twoEdwin Brady 834a5e0Fix bug in applying syntax rulesEdwin Brady b0248eaChecking syntax declarations; also allow symbolsEdwin Brady 2402885Generic syntax declarations (see prelude.idr for example)Edwin Brady 12bd089Added lifting of unsolved metavariables to global functionsEdwin Brady a7d08efdo notation (just IO at the moment - not yet overloadable)Edwin Brady 20861ecEnough Epic to compile 'hello world' (but not much else yet...)Edwin Brady 9d1ecc8Added some syntactic sugar for _|_, () and pairsEdwin Brady