git.iko.soy/Idris-dev
on d676ca6 help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
d676ca6Added -o option, and :exec and :t at the REPLEdwin Brady a4a77bfMake do notation use Monad classEdwin Brady 92bf28eMore name manglingEdwin Brady 27f5a9cFix previous fix ;)Edwin Brady 169d8c0Elaborating instance declarationsEdwin Brady f2459a5Added class constraintsEdwin Brady 13d08bdElaborating class declarationsEdwin Brady 33710abParsing class and instance (but no elaboration yet)Edwin Brady 229a99cBetter elaboration order; also changed instance argument syntax slightlyEdwin Brady 77194b9PatternGuardsEdwin 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 7c4f79cSome progress towards specialisationEdwin Brady 3bdfa26Added [static] annotations (which do nothing yet) and state to evaluatorEdwin Brady 1155e79Laziness annotationsEdwin Brady b8a2bbfAdd :log to REPLEdwin Brady 6757c47Added case analysis on types, but only when enabled with --typecase (since it breaks parametricity)Edwin 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 5f7eed8Propagate line numbers through applications and variablesEdwin Brady ec87a69Some effort at reporting line numbers of errors (top level of decl only)Edwin Brady 070b0faSome unification/evaluation bug fixesEdwin Brady 180e979Added builtins.idr and fixed a bug or twoEdwin 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 ca6a5e1import statementEdwin Brady 083fc70Added 'where' clauses in pattern matchesEdwin Brady de89a04Add ElabInfo to pass through elaboratorEdwin Brady a2a5141Allow interleaving of explicit and implicit arguments in top level typesEdwin Brady a805f47Added constants and some primitive operationsEdwin Brady f9fb363Tinkering with error reportingEdwin Brady 59c1eb1Pretty printing of TT terms as PTermsEdwin Brady 9fe3473Added using blocksEdwin Brady 019fabaFixed unification; added well-typed interpreterEdwin Brady 739e0b5Some error handlingEdwin Brady 22b4dc4Lots of improvements in elaborating and evaluatingEdwin Brady