git.iko.soy/Idris-dev
on 2e02cf6 help sign in
2e02cf6Logging optionsEdwin Brady 74183cbImprove :t for names with implicit argsEdwin 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 285112bNat instancesEdwin Brady a927d65Instances in builtinsEdwin Brady 92bf28eMore name manglingEdwin Brady 27f5a9cFix previous fix ;)Edwin Brady f2368e9More care with naming in where clausesEdwin Brady 814ebdaMake sure patterns are in dependency orderEdwin Brady 169d8c0Elaborating instance declarationsEdwin Brady f2459a5Added class constraintsEdwin Brady 13d08bdElaborating class declarationsEdwin Brady 33710abParsing class and instance (but no elaboration yet)Edwin Brady 27fc1f2Update .cabal and READMEEdwin Brady 5528447Not really mini any more...Edwin Brady df4ee4fMade samples directoryEdwin Brady 229a99cBetter elaboration order; also changed instance argument syntax slightlyEdwin Brady 2d6c12ePrimitive conversion and showingEdwin Brady 77194b9PatternGuardsEdwin Brady ed64e76Better type class resolutionsEdwin Brady 00052c8Ord classEdwin Brady fb233c9Eq class, Nat is a NumEdwin Brady be3a53aType class instance resolution, and some Num overloadingEdwin Brady 429d11aSome help text on :?Edwin 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 f7a7f0bSome proofs in nat.idrEdwin Brady 7b1336bFixed naming problem in type checking of applicationEdwin Brady 58bd7c4Added rewrite tacticEdwin Brady 6cc3c32Fix small elaboration bugEdwin 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 b85965eparser tinkeringEdwin Brady 1155e79Laziness annotationsEdwin Brady 6638f64Some things in the preludeEdwin Brady b8a2bbfAdd :log to REPLEdwin Brady 0eac224Moved primitive operators to builtints.idrEdwin 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