git.iko.soy/Idris-dev
on 43ffd25 help sign in
43ffd25Instance tactic explanationEdwin Brady 535d77bAdd --ibcsubdir option (thanks to Dirk Ullrich)Edwin Brady 6c08816More paper changesEdwin Brady 7e248efMerge branch 'master' of github.com:edwinb/Idris-devEdwin Brady 9bb92a5matchWithEdwin Brady 067f4faUtil.Pretty missingEdwin Brady 08797aeFix bug with de-elaboration of sigma typesEdwin Brady 455ae60Attempt to resolve type classes before applicationEdwin Brady e74e08dMore on elaborationEdwin Brady 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