git.iko.soy/Idris-dev
on 36abfda help sign in
36abfdaElaborating expressionsEdwin Brady a678b80:t prints all names, rather than checking for unique nameEdwin Brady 2037fe8Change precedence of ++ to be higher than ::Edwin Brady 7b10040TinkerEdwin Brady 78f5e62Primitive tactic descriptionsEdwin Brady 4dfa16bMinor rearrangingEdwin Brady eb2c9f9Small paper updatesEdwin Brady 2b5505dA bit on proof stateEdwin Brady 86c5060An elaboration exampleEdwin Brady 4d2f0feMore on the core TTEdwin Brady 8bf44c2More implementation paperEdwin Brady 0af8a2eWork on implementation paper; tutorial fixesEdwin Brady 8d4a93bMerge pull request #17 from dpmulligan/masterEdwin Brady 5602ea7A small cleanup after missing some stray ends in the diff.Dominic Mulligan 2ba8712Merge branches 'improved-pretty-printing' and 'master'Dominic Mulligan 3541c70Merge remote-tracking branch 'upstream/master'Dominic Mulligan 368fdf6Some playing around with widths to make everything look nicer.Dominic Mulligan c824099Major improvement to pretty printing of proof states, especially when the goal is a large term.Dominic Mulligan dca8f9fNormalise types before applying forcingEdwin Brady a94fd81Remove Eq constraint from NumEdwin Brady 8c64e9cGot pretty printing partially working using the Pretty type class as a replacement for Show. Now need to tweak it in order to make everything look nice, and to get terms printing correctly!Dominic Mulligan 7162b6eMerge remote-tracking branch 'upstream/master' into improved-pretty-printingDominic Mulligan f355c72Update dependencies and correct examplesEdwin Brady 02003d7Added malloc and trace_malloc *** This will need the latest EpiVM ***Edwin Brady 637f3bfMerge remote-tracking branch 'upstream/master'Dominic Mulligan 42dcbabMerge remote-tracking branch 'upstream/master' into improved-pretty-printingDominic Mulligan d254ce1Started adding pretty-printing capabilities for core datatypes to improve rendering of proof state.Dominic Mulligan 9a54230Started adding pretty printing capabilities for core data types to improve rendering of proof state.Dominic Mulligan a34b377Added a file for pretty printing arbitrary data types.Dominic Mulligan d466a82Tutorial updatesEdwin Brady 0818a58Merge remote-tracking branch 'upstream/master'Dominic Mulligan 3f13043Make compile time evaluator take advantage of laziness again (And update test001 to catch it if it goes wrong again)Edwin Brady 34459abTest commit after hosing my local copy of the repository through fiddling with git and reverts. Starting on a correctness proof of the heap implementation. Type checking now much faster.Dominic Mulligan 3edef47Fix conflicts and compile errors in recent mergeEdwin Brady 605aea3tinkerEdwin Brady 3ce7d92Better pruning of alternatives so that resolving is much fasterEdwin Brady efc04a3made some instances of complex numbers.Mekeor Melire 7ccc101made Num not a subclass of Ord and Eq, instead only of Eq such that complex numbers, for example, don't have to be ordered.Mekeor Melire a3c760fMerge remote-tracking branch 'upstream/master'Mekeor Melire 58d0a31Merge pull request #16 from dpmulligan/masterEdwin Brady 7559be0An implementation of Okasaki's maxiphobic heaps, along with a derived heap sort algorithm for lists. Performance in this file appears to be a problem, both during type checking and during execution, both in the REPL (divergence) and after compilation (slow, but does seem to work correctly).Dominic Mulligan c31ae84added instance declarations of complex a for class eq and showMekeor Melire 30ca781added complex-module into checkall.idr such that it gets checked, too..Mekeor Melire 7db77dbported Data.Complex from haskell to idrisMekeor Melire ba77a44added a prelude-function "atan2" as in haskellMekeor Melire 8848ad4Merge remote-tracking branch 'upstream/master'Dominic Mulligan 2cde01cMerge branch 'master' of github.com:edwinb/Idris-devEdwin Brady cd38cefEvaluator tinkeringEdwin Brady 651d3afMerge remote-tracking branch 'upstream/master'Dominic Mulligan 4082770Merge pull request #14 from MekeorMelire/masterEdwin Brady