git.iko.soy/Idris-dev
on 4afe404 help sign in
4afe404Fix refine on local namesEdwin Brady e89453fAllow type labels on sigma bindingsEdwin Brady 1c49219Added provisional definitionsEdwin Brady d496a9c:e now reloads the edited fileEdwin Brady e0e52f1simple_app should try both elaboration ordersEdwin Brady f31caf5unique_hole needs to check whole contextEdwin Brady 4931c20Added Integer (but an Epic bug prevents them compiling properly)Edwin Brady e530718Add fromInteger to Nat class; allow type labels on letEdwin Brady 8784b67Int/Float conversion primitivesEdwin Brady f1c7fafAdded tactics construct, and tactic sequencing/choiceEdwin Brady 71c1a0eExtension parsing, now deferring checks name is uniqueEdwin Brady 4a1324cDistinguish term syntax and pattern syntaxEdwin Brady 31d974bMore flexibility with syntax definitionsEdwin Brady c01becbDon't bind pattern variables if they're in scopeEdwin Brady 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