git.iko.soy/Idris-dev
on master help sign in
history of4afe404..master
compare
7315eafAdded a large chunk of theory over lists, most of it taken from the Haskell prelude and the O'Caml standard library.Dominic Mulligan ae4be75Well founded recursion checkEdwin Brady fb3160eTidy up interpreter sampleEdwin Brady dc3f0f9added dsl blocksEdwin Brady c08dff7Fix circular dependenciesEdwin Brady 6a5d1fcMerge pull request #2 from dpmulligan/masterEdwin Brady b63e9bbMerge pull request #3 from nlogax/masterEdwin Brady 6807cf4Unreachable case warningEdwin Brady 64a2bc8Add `head` and `tail` for listsJonas Westerlund 12c93edUpdate to Setup,hs (via Dirk Ullrich)Edwin Brady 5570ceeRe-added missing maybe_bind to prelude Maybe module.Dominic Mulligan d282d56Forgotten a fix to catMaybes which was pattern matching against an Either type, not the Maybe type.Dominic Mulligan 1ea1993Changes to prelude Maybe.idr file: removing class instances that were already defined, as well as fixing a type error.Dominic Mulligan 2f5f607Merge remote-tracking branch 'upstream/master'Dominic Mulligan 34b88d6Added more to prelude, specifically in the files either.idr and maybe.idr. Ported most of the (total functions from) the Haskell Prelude relating to these types, as well as commonly used auxilliary functions found in third-party libraries on Hackage.Dominic Mulligan c67c3f1Merge pull request #1 from dpmulligan/masterEdwin Brady 247b20cSome minor fiddlingEdwin Brady 126ab04added a gtksourceview-2.0 and gtksourceview-3.0 idris language highlighting grammar for use with gedit and other gnome based text editors. used the existing haskell language specification as a baseDominic Mulligan e39254cAdded 'abandon' command in proof mode (Alternatively, :q)Edwin Brady eec2b83Fix syntax macro bugEdwin Brady 401e9a0so type and pattern/term syntax extensions in tutorialEdwin Brady 3b36802Record syntax (but no magic yet...)Edwin Brady 3b13341Better error reporting for unresolved type classesEdwin Brady 4c3fb9bAnother cabal fixEdwin Brady 1d76cd3Fix checked vs inferred bugEdwin Brady 566616cFixed bug: global names should not override 'using' namesEdwin Brady 95ff97cFix bug: checking names are not local before adding implicits and resolving namespacesEdwin Brady 6611494Fix for install with latest cabalEdwin Brady c613fabUpdate tutorialEdwin Brady 6682ebbPropagate solutions properlyEdwin Brady 991c229Better match checkingEdwin Brady a3c6231:addproof knows about .lidr filesEdwin Brady 558d226Update elaborator for application of local variablesEdwin Brady 22f40c1Update CHANGELOGEdwin Brady 0a61aa0Update tutorialEdwin Brady 7df6265Remove some needless bracketing from if...then...elseEdwin Brady 33bf2bdUnification tweakEdwin Brady 5ef6475Tutorial typosEdwin Brady d1d672eCollect all unification errors instead of immediately reporting failureEdwin Brady ce10256Tutorial typosEdwin Brady 856f142Fixed VNil in tutorial (well spotted Cezar :))Edwin Brady 6e699c7Add Transform module; make implicit args lazyEdwin Brady ae47b8fMinor tutorial changesEdwin Brady 9538419Update descriptionEdwin Brady b47740dcabal changesEdwin Brady 1112fe4Coverage checker Not quite complete - a bug (which I know how to fix) makes some things appear not covering even though they are. Results currently used only for pruning case trees in compiled code. There is a small performance penalty - coverage checking can be disable with --nocoverageEdwin Brady 3f18d02Record data type infoEdwin Brady 38732d8Heuristic for picking best error message when overloaded alternatives all failEdwin Brady 10ea548Inline type class applications where possible to reduce overheadEdwin Brady 42ca063:d to display elaborated pattern definitionEdwin Brady