git.iko.soy/Idris-dev
on master help sign in
history of814ebda..master
compare
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 54cbf2fjavascript: added required decl for browsersraichoo a4178c0javascript: fixed broken mergeraichoo f868390Magic with explanation in impl-paperEdwin Brady d737d67Small library tweaks and documentation updateEdwin Brady a76f8b3More sane scoping rules for where/type classes Parameters in the type signature get propagated, indices do not. So you no longer need to pass parameters explicitly if you need them in a where clause, and you no longer need to give explicitly typed helpers in type class instances for types with indices.Edwin Brady 75e7758Some progress on implementation paper revisionsEdwin Brady 2a13be4Distinguish parameters and indices internally in data types This doesn't do anything, yet, but will become important soon!Edwin Brady d02610ajavascript: special handling for space and underscore in identifiersraichoo fe570cbjavascript: filter all nonascii letters from identifiersraichoo 2407cbbjavascript: check for keywords as identifiersraichoo e5706d3HNF in unification to speed things upEdwin Brady 3a27fdeArguments under type constructors are not forceable!Edwin Brady 92257c4Fix mysterious "no such variable" bugEdwin Brady 67de7f7Add a reducing version of believe_me (be careful!)Edwin Brady 8f76315Changed approach to unification Instead of failing immediately, maintain a list of blocked problems and refine during elaboration.Edwin Brady 4a15c64Fix samples to use Type instead of SetFrederic Koehler