git.iko.soy/Idris-dev
on master help sign in
history of019faba..master
compare
5f6ac67In-lang stringification of BitsBenjamin Saunders 1ffdfc0Parse case options as patterns, not expressions Fixes issue #147Edwin Brady 9909d70More concise (and less fragile) boolean comparison wrappersBenjamin Saunders 358c623Partially restore access qualifiersBenjamin Saunders da79c5eComparisons on bitsBenjamin Saunders ee40d17Strip access qualifiers pending resolution of issue #143Benjamin Saunders 57628ffMerge pull request #146 from raichoo/javascriptEdwin Brady 59be497javascript backendraichoo 6322cc6Merge pull request #141 from sanxiyn/masterEdwin Brady b2cf967Allow class constraints in syntax definitionsEdwin Brady c3cb8a4Correct module namesBenjamin Saunders 04d6f00A small amount of proof automation, via tactic reflectionEdwin Brady d06d473Fix injectivity checkEdwin Brady 25ec644Modify documentation comment parsingEdwin Brady 2308c53More optimization-friendly intToBitsBenjamin Saunders 88eb2bfC codegen for bitmanip and bit comparatorsErkin Batu Altunbaş ebacfeeEquality result typeBenjamin Saunders df10078Complement primitive for bit typesBenjamin Saunders 12615d4Swapped bitsEq Either ordering to be in the spirit of Right=successBenjamin Saunders c3f27f7Safe bitsEqBenjamin Saunders 927fd18Machine integer comparison primitives and a proofy interface to the equality caseBenjamin Saunders 0b96076Cast instances for Mod2 <=> Bits and Int => BitsBenjamin Saunders ef96397Replace general modulo type with modulo 2^n typeBenjamin Saunders 1006d3aCorrect behavior of operations on non-native bit widthsBenjamin Saunders 5a26a74Show instance for ModuloBenjamin Saunders 279b02dAccess qualifiers for ModuloBenjamin Saunders 8252b94Strongly-typed bitsBenjamin Saunders 001469dCast Int (Bits n) instanceBenjamin Saunders 8216c7fBasic bit-twiddling primitivesBenjamin Saunders 348cf91String primitivesBenjamin Saunders 0045b68Resolve implicit definition warnings relating to bitstringsBenjamin Saunders 5734ddfBeginnings of generic machine integer supportBenjamin Saunders e2807a1Verified numbersBenjamin Saunders b3ba46ePrimitives for interconversion of Bits32 and IntBenjamin Saunders 103d65eflooring log2 for NatsBenjamin Saunders 7518b0cAbsolutely untested implementations of a few bitstring primitives.Irene Knapp b896224Primitive types for groups of 8, 16, 32, and 64 bits, and basic arithmetic and mutual conversion operations on themBenjamin Saunders d95a981Transitivity of equalitySeo Sanghyeon 4bc6424Compile on GHC 7.0Seo Sanghyeon 12dcee5Merge commit '06fffa315afc0d883f36a6ce971df1123aa6d8e3' into javascriptIrene Knapp 06fffa3JavaScript stuff.Irene Knapp 60dbc48Add %instance for explicit access to resolveTC tacticEdwin Brady bfd5b51Make sure names are not defined more than once Fixes issue #124Edwin Brady 496cf41Abstract from everything to make 'with' more magicEdwin Brady 8d83f38Abstract matched terms from goal type in with clauses (like 'magic with' in Agda)Edwin Brady 11dbfc0Correct totality check of f=f, and add regression testEdwin Brady bc3e807Merge pull request #136 from DanielWaterworth/useful_functionsEdwin Brady 28b68fdMerge pull request #135 from DanielWaterworth/masterEdwin Brady 449e292Tweak totality checkerEdwin Brady 906862aFix traversal of size change graphs Fixes issue #134 - new regression test addedEdwin Brady