git.iko.soy/Idris-dev
on 0bc69fb help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
11d4feeSome file handlingEdwin Brady 87946abShow user chosen names rather than machine onesEdwin Brady dea8d48Added support for literate programming with bird tracks (use .lidr extension)Edwin Brady dccbc43Generate bytecode so that files don't need to be rechecked every time they're loadedEdwin Brady 8f77986Added some serialisationEdwin Brady 60c4ef9Added 'impossible' keywordEdwin Brady 3b5e50cAdded universe constraint checker and --typeintype command line optionEdwin Brady f2e3a76Default definitions in classes, plus some bug fixingEdwin Brady acb1f19Add :a comment, to add most recent proof script to source fileEdwin Brady 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