on master help sign in
history of09f2abd..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