git.iko.soy/Idris-dev
on 6bef4f9 help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
fa5f1cdNamespacesEdwin Brady 8cd093fChanged lookup to return a list (preparation for namespaces)Edwin Brady 94d888bParsing and elaboration of alternativesEdwin Brady ada02deTinker with universe constraintsEdwin Brady 5b08cc9Add PAlternativeEdwin Brady b26716aCollect cumulativity constraints on universesEdwin Brady 01ceeadNamesEdwin Brady e473c2eExists namingEdwin Brady bd793e2Better elaboration of Sigma (for better error messages)Edwin Brady bbaa193Better representation of namesEdwin Brady 93946fcinsertImpl shouldn't crash if given too many argumentsEdwin Brady 925648aAdd %include directiveEdwin Brady 374fc26Add let x = t tacticEdwin Brady df49a2awith fixEdwin Brady 048e2a7namesIn should look for *all* namesEdwin Brady 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