git.iko.soy/Idris-dev
on master help sign in
history of43ffd25..master
compare
4fc1cbdMerge pull request #110 from LeifW/platform_agnosticEdwin Brady 06283b6Improve evaluation of projection By caching result of evaluation, so that it's already evaluated when next projection happens.Edwin Brady 2f26fb2Add Debug.TraceEdwin Brady 0c8d6e7Merge pull request #112 from raichoo/masterEdwin Brady e0d0b13added Data.Bits and primitives for Intraichoo 20627e4Better strategy for building case trees at compile timeEdwin Brady 0136305Add bitwise &/| primitives for Int (prim__andInt / prim__orInt)Edwin Brady fd5cddbMore platform agnostic nowChetan T 7fe382dFix Unlit to cope with documentation comment syntaxEdwin Brady 32c8104Fix scoping error in proof scripts Fixes issue #106Edwin Brady 817211aUndo a change in error rendering that was only for debugging...Edwin Brady 1738775Check result of elaboration at the REPL properlyEdwin Brady 3187e59Merge pull request #108 from bitlisp/masterEdwin Brady 5501396'the' function for inline type annotationsBenjamin Saunders f9e0605Change to Util.System for portabilityEdwin Brady 5138f54Merge pull request #104 from LeifW/make_idris_install_respect_targetEdwin Brady 04650f0Merge pull request #105 from chetant/windowsEdwin Brady 960c468Tutorial updates Note on local type inference in 'where', and 'mutual' blocks.Edwin Brady 4a9c0f4Fix argument names in generated types for where blocksEdwin Brady 979520bUpdate CHANGELOGEdwin Brady c10146bLimited type inference of types in where clauses Type signatures can now be omitted *only* if the type of the function can be determined completely from the first call.Edwin Brady aa7262ePut deferred names in the right namespaceEdwin Brady f833918(Experimental) Create deferred definitions by applicationEdwin Brady e23c029Allow type annotations on let tacticEdwin Brady 614c682Fully compiles and tests under windows mingw32Chetan T 81d917fAllow $TARGET to override libdir on the `idris --install` command.Leif Warner 9db94c0Merge branch 'master' of https://github.com/edwinb/Idris-dev into windowsChetan T 01d6e28Ignore windows test binariesChetan T 1d0c6aaFixing compilation in Mingw32Chetan T 160eeddMerge pull request #101 from chetant/windowsEdwin Brady 7c71bfaMerge branch 'master' of https://github.com/edwinb/Idris-dev into windowsChetan T 51f3340Merge pull request #99 from raichoo/masterEdwin Brady d9d8968Merge pull request #100 from raichoo/vimEdwin Brady bb9a3adtypo fix in git attributes, adding test results to gitignorechetant fab5d73Adding support for Windows MingW32chetant af66f58vim: added postulate to highlighterraichoo 430eab9Allow postulates in where/parameters blocksEdwin Brady b1cdd04Added postulate declarations postulate foo : type -- 'type' must return something of a collapsible type, i.e. a type with at most one instancei determined entirely by the indices, to ensure that it is unused at run-time.Edwin Brady 1f98328fixed non-exhaustive clause with guardraichoo 2250085indent fixity error messageraichoo 5d33da2removed "user error" from error messagesraichoo a6f8de5Fix name shadowing bug in case/destructuring let Fixes issue #96Edwin Brady e7c9256Allow inference of Sets at REPLEdwin Brady 50d93dcFix tutorial typoEdwin Brady c71ce04Marginally improve unification errorsEdwin Brady 9a444c5Add 'mod' and variantsEdwin Brady 1b3f4edClearer type class errors Method cannot be used in a type declaration in the class in which it is defined, as the class definition is not yet complete.Edwin Brady bc37932Add Fin.strengthenEdwin Brady af71c77Bring CHANGELOG up to dateEdwin Brady 1677c30Better dealing with name shadowing while building instances ...and while type checking completed termsEdwin Brady