on master help sign in
history of4afe404..master
compare
dc67893Remove some unused codeEdwin Brady ac05da7Added Semigroup and Monoid instances (non-verified) to list module.Dominic Mulligan b87be34Some minor shuffling of proofs to make it easier to see what has been proved.Dominic Mulligan b7f6d0fAdded zip and unzip functions to list module, upto zip3 and unzip3.Dominic Mulligan b1a5da4Merge remote-tracking branch 'upstream/master'Dominic Mulligan 7e75eadMissing .tex filesEdwin Brady 76ac83bParse rule for big integers is brokenEdwin Brady 0607514Merge pull request #12 from tomprince/cabal-installEdwin Brady b265313Take and drop ported from list library to vectors. Function catMaybes causes Idris to diverge upon type checking in the REPL.Dominic Mulligan 74a25e8Rewrite cabal config to be distribution friendly.Tom Prince 97e28f7Export tactic-implicit arguments properlyEdwin Brady c887611Merge pull request #11 from dpmulligan/masterEdwin Brady 02ef050Ported the majority of the list API to the vector data type.Dominic Mulligan 1e6c93cAdditions to the vect.idr file.Dominic Mulligan 9489bb0Fix take/dropEdwin Brady bbb978bSet up .bibEdwin Brady 7cca84fMerge pull request #10 from dpmulligan/masterEdwin Brady 5521977Small changes fixing typos.Dominic Mulligan 29f89d1First attempt at the "shadow" numeric hierarchy with properties enforced by the type system.Dominic Mulligan bc983bbFixed broken instances following e-mail conversation with Edwin in nat.idr. Changed fixity of semigroup and group operators from right to left.Dominic Mulligan 0432a70Check that methods are part of a class when defining instancesEdwin Brady a87be32Merge pull request #9 from dpmulligan/masterEdwin Brady dcba960Better way of pruning type class searchEdwin Brady 066b356Fix to get the nat.idr file working correctly. Some sort of bug or misunderstanding in how infix operators are being exported from the algebra.idr file.Dominic Mulligan 3900c38Added more algebraic structures to the lib/prelude/algebra.idr. Also useful for debugging typeclasses.Dominic Mulligan 92d99f8Chase type classes for longerEdwin Brady 463e62aSome type class bug fixesEdwin Brady 7c42f77update algebra.idrEdwin Brady 9f842bdMerge pull request #8 from dpmulligan/masterEdwin Brady e4cefe8Oops: mistakenly reverted to faulty definition of Eq on nats.Dominic Mulligan 7f7cf8cA few changes:Dominic Mulligan 891b52a%obj should be %link in tutorialEdwin Brady cb47ec1record fixEdwin Brady 81f2c89Small error message fixEdwin Brady 4bcfa68Tinker with specialisationEdwin Brady 09f2abdFix let overloading bug with do blocksEdwin Brady 0338d39Fix case statements in type signaturesEdwin Brady 00d7c69Work towards making {static} arguments and specialisation work properlyEdwin Brady ae1cf53Tutorial typos fixedEdwin Brady 5399670Some documentation updatesEdwin Brady 709e330Check for overlapping type class instancesEdwin Brady 58bcd1eBetter type class resolutionEdwin Brady 33baa44More on errors; propagate line numbersEdwin Brady ed72247Try to get line numbers betterEdwin Brady b04ea13Eq Nat fixEdwin Brady c7a3b59Coverage checker tweakEdwin Brady f49cd3bPass options on functions in typeclasses through to instancesEdwin Brady 6b6dc72Added note on the empty type and totality checking to the tutorialEdwin Brady 9839562Fix silly error in termination checker :)Edwin Brady 86c2beeMerge pull request #7 from dpmulligan/masterEdwin Brady