git.iko.soy/Idris-dev
on 895e66f help sign in
895e66fType class resolution when there is inheritanceEdwin Brady 01ceeadNamesEdwin Brady 03d7d5eAllow type labels on lambdasEdwin Brady dbc607cDecorating names for namespacesEdwin Brady e473c2eExists namingEdwin Brady e713a98getWitness/getProofEdwin Brady bd793e2Better elaboration of Sigma (for better error messages)Edwin Brady 1807c65No letters in operatorsEdwin Brady bbaa193Better representation of namesEdwin Brady 34f92f3Fix deferred names in type declarationsEdwin Brady f9a0008Added 'believe_me'Edwin Brady ae3ad10Apply fromInteger for negative numbersEdwin Brady 325b919:t for names as well as termsEdwin Brady e20f401No holes allowedEdwin Brady 93946fcinsertImpl shouldn't crash if given too many argumentsEdwin Brady 925648aAdd %include directiveEdwin Brady 663c464Added test directory and a single test...Edwin Brady 374fc26Add let x = t tacticEdwin Brady df49a2awith fixEdwin Brady be2d7faCtrl-D now quits replEdwin Brady 9a59cb5Add FalseElim as a primitiveEdwin Brady da5e25eeither.idrEdwin Brady 8d83d07Type declarations of the form (x,y,z : A) -> BEdwin Brady 1309a42Give pi bindings unique namesEdwin Brady 048e2a7namesIn should look for *all* namesEdwin Brady 04ac1a8/= for FinEdwin Brady 72c2e2aEquality on FinEdwin Brady 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