git.iko.soy/Idris-dev
on master help sign in
history of4d2f0fe..master
compare
5b12933Corrected typo of the (++) example in views.textauli 2a97d54Make seperated named functions for the Monoid <=> Maybe cast.Leif Warner 14cce81Normalise before looking for coercionsEdwin Brady 465acafRewrite Prelude.Vect.zip in terms of Prelude.Vect.zipWithMelvar Chen 9c77928Add zipWith, concat, and deleteAt to Prelude.VectMelvar Chen 34909f5Merge pull request #202 from DanielWaterworth/masterEdwin Brady a5ea29fMerge pull request #203 from david-christiansen/haddockEdwin Brady 422521fTweak syntax rules to deal with consecutive non-terminals betterEdwin Brady 22c355aDocumentation comment additionsDavid Christiansen c0bc353Build Haddock and Hoogle filesDavid Christiansen 48c4793Added curry and uncurry functionsDaniel Waterworth 195e30bMerge pull request #200 from raichoo/masterEdwin Brady f29a167added Eq typeclass for Mayberaichoo 25b4dd1Merge pull request #198 from david-christiansen/readmeEdwin Brady cbaf2f8Added testing instructions to READMEDavid Christiansen dc52276Add Decidable directory to idris.cabalEdwin Brady 1898213Merge branch 'master' of github.com:edwinb/Idris-devEdwin Brady f44e1d7Merge pull request #193 from david-christiansen/decidableEdwin Brady ff2a2a7Merge branch 'master' of github.com:edwinb/Idris-devEdwin Brady 318e20dMerge pull request #197 from david-christiansen/haddockEdwin Brady 4187c57Add Catchable and IOExcept modulesEdwin Brady 306a451Reformat existing comments for Haddock and add Haddock commentsDavid Christiansen 1e86384Haddock for completion moduleDavid Christiansen adf51f4Make Haddock able to parse Idris's sourceDavid Christiansen f8e41c5Fix error with coercions in function argumentsEdwin Brady 15cdb1aMerge branch 'master' of github.com:edwinb/Idris-devEdwin Brady 98599b5Only apply unique implicit conversions (and add test)Edwin Brady 728f9a2Merge pull request #196 from raichoo/masterEdwin Brady 28d9472vim: added implicit and static annotationsraichoo d13941cUpdate tutorialEdwin Brady f46aacdBrief note on implicits in the tutorialEdwin Brady 022d4dfAdded 'implicit' conversions implicit f : a -> b Then, when a function needs a 'b' but has an 'a', f will be called implicitly. This is probably scary and fragile. Use with extreme caution!Edwin Brady e81be38Remove misplaced instanceDavid Christiansen b92b12eAdded typeclass for decidable equality plus instances for commonly-used datatypesDavid Christiansen decad94Decidable predicate ADTBenjamin Saunders 095301fAdd missing modules to idris.cabalEdwin Brady 82a4e9bFix for line numbers on type signaturesEdwin Brady 2396796Merge branch 'javascript' of https://github.com/raichoo/Idris-dev into raichoo-javascriptEdwin Brady 12189d7Normalise type before checking it's a valid postulateEdwin Brady b2f2be4javascript: extracted common runtimeraichoo 2b09cc1Increment IBC versionEdwin Brady b35df0dMerge branch 'bitstring' of https://github.com/bitlisp/Idris-dev into bitlisp-bitstringEdwin Brady 7e12b2aUpdate version to 0.9.6.1Edwin Brady e2809b6Fix non-termination error in universe checkerEdwin Brady 06bfa75Fix error in conversion check Fixes issue #187Edwin Brady 4e19c35Make coverage checker a lot faster ...with strategic use of 'nub' so as not to generate a crazy number of clauses!Edwin Brady 4c45c09Speed up termination checker Lots of duplication of work was happening, both ignoring functions that were already known to be total, and repeating checks when arguments not decreasing, now pruned.Edwin Brady 296588fRevision of impl-paper completed.Edwin Brady 091a5dfSome polishing, spell checkingEdwin Brady 99bc1d5Merge pull request #186 from ggreif/patch-1Edwin Brady