git.iko.soy/Idris-dev
on 64a2bc8 help sign in
64a2bc8Add `head` and `tail` for listsJonas Westerlund 12c93edUpdate to Setup,hs (via Dirk Ullrich)Edwin Brady 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 baaba44Run-time forcing optimisationEdwin Brady 02881b1Implemented forcing optimisation Constructor arguments which are inferrable from the indices in the constructor type are erased both at compile-time and run-timeEdwin Brady 19f1e3aCompatibility with old ghcEdwin Brady c82f2f4Add nullPtr/validFileEdwin Brady 969e573Checking elaborated term and inferred term matchEdwin Brady 3af0ae0Elaborator tweak, dealing better with values that are inferred automaticallyEdwin Brady 22b2879Making IO lazy means we need to force an evaluation for anything to happen at all...Edwin Brady 598160cMake foreign calls lazily (or they get executed at the wrong time...)Edwin Brady f3ce933Some prelude shufflingEdwin Brady 2ce525eintros tactic; some library tinkeringEdwin Brady a33b4c2Avoid adding duplicate information to .ibc => quicker load timeEdwin Brady 201ade9Fixed accessibility bug; added some library functionsEdwin Brady 0b9cab2Note on cumulativity in tutorialEdwin Brady