on cd92ae8 help sign in
cd92ae8Namespaces only containing private members is now correctly considered emptyPhilip Rasmussen 940da80Merge remote-tracking branch 'upstream/master' into idrisdocPhilip Rasmussen fd1219bMerge pull request #1130 from jonsterling/fix/reify-intro-inductionEdwin Brady 4ed706aMerge pull request #1125 from david-christiansen/lidrEdwin Brady 1a9ab34Merge pull request #1119 from KesterTong/fix/master/randomEdwin Brady 5850126Merge pull request #1124 from raichoo/javascriptraichoo dc0332fMerge pull request #1116 from ziman/fix-cplxEdwin Brady c0e6c24Merge pull request #1115 from puffnfresh/bug-fixesEdwin Brady 4aec152Added more HaddockPhilip Rasmussen 35a2187Added Haddock to a functionPhilip Rasmussen 0cb6c65:makewith works with .lidr nowDavid Raymond Christiansen abd5f0cremove javascript lib in favor of idris-hacker/iQueryraichoo b16871fAdds Google to contributors listKester Tong 90bad48Refactors rndFin' to only accept length > 0 vectorsKester Tong 31b48edAdds rndSelectKester Tong 5ded2c1Adds docstringsKester Tong 90aa3d8Fix addition and subtraction of Complex Float.Matus Tejiscak d773ae8Remove whitespace for :addproof - like :load doesBrian McKenna ce9afaeMakes rndFin take all values in Fin (S k)Kester Tong 62705e4Tweak mergeNotunifiedEdwin Brady 70e9dc9Merge pull request #1112 from PhilipRasmussen/idrisdocEdwin Brady 86b2ef4Merge pull request #1107 from ziman/data-erasedEdwin Brady 198d067Merge pull request #1106 from ziman/fix-dctor-erasureEdwin Brady 1adeea3Merge pull request #1105 from ahmadsalim/improvement/refactorpisEdwin Brady 74539a5IdrisDoc now merges documentation more robustly using less code.Philip Rasmussen 6bc9957Fixed typoPhilip Rasmussen 1f6e885Fixes a problem with custom tactics using Intro & InductionJonathan Sterling dd6b95aRemove trailing whitespace.Matus Tejiscak 27cd063Add a regression test.Matus Tejiscak e2249c0Add workaround for some non-trivial case-matches on detaggable data.Matus Tejiscak 3aa1833Add Data.Erased to libs/base.Matus Tejiscak d7e4bfaFix indentation.Matus Tejiscak fb3d76cAdd a check for missed newtype optimisations.Matus Tejiscak 8e3d3c0Fix erasure from data constructors.Matus Tejiscak e9127baRestored "__pi_arg" to use UN instead of MN again (due to a test failure). Removed commented out code.Ahmad Salim Al-Sibahi 7ed177aBetter error for ambiguous instance nameEdwin Brady f2bf55dMerge 'not unified' variablesEdwin Brady d28c82fRefactor parsing of Pi/Dependent Type Signature expressions to improve error reporting and reduce lookahead.Ahmad Salim Al-Sibahi 51394aaAdd 'unify' tacticEdwin Brady 601342ftrans doesn't need homogeneous equalitiesEdwin Brady e28fbb1Merge pull request #1104 from puffnfresh/docsEdwin Brady 074e10bMerge pull request #1103 from PhilipRasmussen/idrisdocEdwin Brady 3badee5Merge pull request #1097 from david-christiansen/pprintEdwin Brady 140d8d2Add check after each proof step, not just the endEdwin Brady e202cfdMade test resistant to differences among command implementationsPhilip Rasmussen ab6de0eChanged test implementationPhilip Rasmussen 31c4938Added missing test directoryPhilip Rasmussen 079856cRemoved test backups and converted tests to pure bash scriptsPhilip Rasmussen 3146e46Rewrote 'expected' filePhilip Rasmussen 6f08060Added IdrisDoc testsPhilip Rasmussen