git.iko.soy/Idris-dev
on master help sign in
history off97602b..master
compare
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 1819feamade TOC in tutorial clickable but still without colorMekeor Melire 14955ffMerge remote-tracking branch 'upstream/master'Dominic Mulligan c666be8Added prim__bigIntToInt (needs latest EpiVM)Edwin Brady 1c2098aAdded infinite list syntax [1..], [1,3,...] etc (But it doesn't work at the REPL yet because that doesn't respect 'lazy' annotations properly)Edwin Brady 022e230Added backtick notation: e.g. x xsEdwin Brady a12ecc2Fix parser bug: whitespace now allowed at the top of modulesEdwin Brady a5b7eedAdded a 'boredom threshold' to the evaluator If it takes too long (probably because it's evaluating a non-terminating function) just returns the input. This is hopefully temporary until the totality checker works better...Edwin Brady 8c29ac4Merge remote-tracking branch 'upstream/master'Dominic Mulligan 15524a8Merge pull request #13 from dpmulligan/masterEdwin Brady 4a7ed14Merge remote-tracking branch 'upstream/master'Dominic Mulligan ab039f2Fix universe checking bugEdwin Brady f4b7e9bMerge remote-tracking branch 'upstream/master'Dominic Mulligan 24d95b0Added mconcat for concatenating over an arbitrary monoid (replace concat on lists with the generalized version later?)Dominic Mulligan