git.iko.soy/Idris-dev
on 4187c57 help sign in
4187c57Add Catchable and IOExcept modulesEdwin Brady f8e41c5Fix error with coercions in function argumentsEdwin Brady 15cdb1aMerge branch 'master' of github.com:edwinb/Idris-devEdwin Brady 98599b5Only apply unique implicit conversions (and add test)Edwin Brady 728f9a2Merge pull request #196 from raichoo/masterEdwin Brady 28d9472vim: added implicit and static annotationsraichoo d13941cUpdate tutorialEdwin Brady f46aacdBrief note on implicits in the tutorialEdwin Brady 022d4dfAdded 'implicit' conversions implicit f : a -> b Then, when a function needs a 'b' but has an 'a', f will be called implicitly. This is probably scary and fragile. Use with extreme caution!Edwin Brady 095301fAdd missing modules to idris.cabalEdwin Brady 82a4e9bFix for line numbers on type signaturesEdwin Brady 2396796Merge branch 'javascript' of https://github.com/raichoo/Idris-dev into raichoo-javascriptEdwin Brady 12189d7Normalise type before checking it's a valid postulateEdwin Brady b2f2be4javascript: extracted common runtimeraichoo 2b09cc1Increment IBC versionEdwin Brady b35df0dMerge branch 'bitstring' of https://github.com/bitlisp/Idris-dev into bitlisp-bitstringEdwin Brady 7e12b2aUpdate version to 0.9.6.1Edwin Brady e2809b6Fix non-termination error in universe checkerEdwin Brady 06bfa75Fix error in conversion check Fixes issue #187Edwin Brady 4e19c35Make coverage checker a lot faster ...with strategic use of 'nub' so as not to generate a crazy number of clauses!Edwin Brady 4c45c09Speed up termination checker Lots of duplication of work was happening, both ignoring functions that were already known to be total, and repeating checks when arguments not decreasing, now pruned.Edwin Brady 296588fRevision of impl-paper completed.Edwin Brady 091a5dfSome polishing, spell checkingEdwin Brady 99bc1d5Merge pull request #186 from ggreif/patch-1Edwin Brady 5bfda79removed extra "this"Gabor Greif 7574d09Lots of implementation paper revisionsEdwin Brady c020e50javascript: split javascript and node targetraichoo a9d6518Move bitstring stuff to Data to reduce potential for name clashesBenjamin Saunders 4c5b1bdMerge branch 'master' into bitstringBenjamin Saunders f31c76aMerge branch 'master' of github.com:edwinb/Idris-devEdwin Brady 1eed9c2Merge pull request #181 from raichoo/masterEdwin Brady d53fccfMerge pull request #180 from david-christiansen/completion-workEdwin Brady 053708aMerge pull request #176 from david-christiansen/completionEdwin Brady a6c36d3Undo previous change until I work out why it was important...Edwin Brady 37ed162load command should ignore trailing whitespacesraichoo bdf07beManually track prover historyDavid Christiansen 66d8360Crude support for completion in proverDavid Christiansen 52203a3Complete tactic names in proverDavid Christiansen cc80288Rename the REPL's Haskeline uses to make them obviously REPL-specificDavid Christiansen 0970f01Disentangle Haskeline from the internals IdrisDavid Christiansen cc3c913Complete arguments of commands (though slightly crudely)David Christiansen f0e096bComplete multiple identifiers in one expressionDavid Christiansen fc58a50Simple completion supportDavid Christiansen 4ae0450Remove old code, tinker with section 4Edwin Brady 2b3634aTinker with spacingEdwin Brady fe89d0dMore on related workEdwin Brady 8843539Tinkering with related workEdwin Brady 22316d9Show how tactics are applied in impl-paperEdwin Brady 9ffcfb8Add Unify details in impl-paperEdwin Brady 48b3618Added metatheoretic propertiesEdwin Brady