git.iko.soy/Idris-dev
on ed64e76 help sign in
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 bf368abFirst attempt at with ruleEdwin Brady cc4eb28let bindings; fixed bug with simple lambda appEdwin Brady 796fa25BannerEdwin Brady 5f7eed8Propagate line numbers through applications and variablesEdwin Brady ec87a69Some effort at reporting line numbers of errors (top level of decl only)Edwin Brady 2c4ff83Change unification in function applicationsEdwin Brady 070b0faSome unification/evaluation bug fixesEdwin Brady 180e979Added builtins.idr and fixed a bug or twoEdwin Brady 834a5e0Fix bug in applying syntax rulesEdwin Brady b0248eaChecking syntax declarations; also allow symbolsEdwin Brady 2402885Generic syntax declarations (see prelude.idr for example)Edwin Brady 12bd089Added lifting of unsolved metavariables to global functionsEdwin Brady 7ea4422added vect.idrEdwin Brady a7d08efdo notation (just IO at the moment - not yet overloadable)Edwin Brady 1c9392etinker tinkerEdwin Brady bda1f6fMore of the compilerEdwin Brady 4436bcbAdded Idris.CompilerEdwin Brady 20861ecEnough Epic to compile 'hello world' (but not much else yet...)Edwin Brady 38a6bc7Added some library filesEdwin Brady 9d1ecc8Added some syntactic sugar for _|_, () and pairsEdwin Brady 868409aSmall bug fixesEdwin Brady bcdde4aMakefile addedEdwin Brady f208c49Library checkingEdwin Brady