git.iko.soy/Idris-dev
on decad94 help sign in
decad94Decidable predicate ADTBenjamin Saunders 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 528c4b4Note on metatheoryEdwin Brady 0d11515Lots of implementation paper revisionEdwin Brady e49ab72Reorder the monad transformers in the Idris monad to allow completionDavid Christiansen 940a7a9Fix compile warning in ElabDeclsEdwin Brady 25cd881Merge branch 'master' of github.com:edwinb/Idris-devEdwin Brady 3c6fe06Error handling interpreter needs Functor instance (via bishboria)Edwin Brady 3dd89ebMerge pull request #173 from raichoo/javascriptEdwin Brady 73ec76fMerge pull request #170 from frytvm/masterEdwin Brady