git.iko.soy/Idris-dev
on 4afe404 help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
e89453fAllow type labels on sigma bindingsEdwin Brady f1c7fafAdded tactics construct, and tactic sequencing/choiceEdwin Brady 4a1324cDistinguish term syntax and pattern syntaxEdwin Brady c01becbDon't bind pattern variables if they're in scopeEdwin Brady 5afe678Added log/exp (and lib/link directives)Edwin Brady 2c05448Give invented pattern variables unique namesEdwin Brady ffc64e3Add mechanism for simplification and function optionsEdwin Brady 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