git.iko.soy/Idris-dev
on master help sign in
history of0abbd53..master
compare
134eef4somethingBenjamin Saunders 58f3f68Merge branch 'master' of github.com:edwinb/Idris-devEdwin Brady c7fded1Added 'mrefine' tactic Like refine, but uses matching instead of unification to resolve implicit arguments. All will become clear, I hope :). This is intended for an additional style of pattern matching (on types) for better explanation of proofs.Edwin Brady 31f4e9fAdd bash completion file for IdrisIgnas Vyšniauskas 115783cMerge pull request #351 from Melvar/hvectEdwin Brady fbc56a0Merge pull request #350 from david-christiansen/prim-annotationsEdwin Brady 1e40959Merge pull request #349 from david-christiansen/haddockEdwin Brady 8b38063Merge pull request #346 from bitlisp/fixed-bigint-truncEdwin Brady e221d08Merge pull request #344 from andy-morris/commentEdwin Brady 357e6b1Merge pull request #345 from david-christiansen/executor-primitivesEdwin Brady eb08982Make 'repeat' run lazily Needs 'lazy' in the recursive call otherwise it will run forever when compiled. Fixes issue #352Edwin Brady e87a7aeMake additions public and require totalityMelvar Chen c5979f4Add type-directed HVect functions and supporting Elem functionsMelvar Chen affd239Add type annotations to Primitives.hs to aid in understandingDavid Christiansen ddaf6b6Fix Haddock parser errorDavid Christiansen 9324eebadd Data.HVectMelvar Chen 10da5a2Fix truncation of Integer in C codegenBenjamin Saunders 53ced7bExtract getOp to top level defnDavid Christiansen 184e27aAdded the rest of the primitives to the executorDavid Christiansen 67e7b00All primitives through SDavid Christiansen 73eb351Primitives a-l doneDavid Christiansen 77ba946Primitives a-g definedDavid Christiansen 01283ecFloat primitivesDavid Christiansen a2ba532All primitives through equalityDavid Christiansen 5fc4278Add all and primitives to the executorDavid Christiansen 0daed45All add primitives present in executorDavid Christiansen 5a968c4Parse empty commentsAndy Morris 1b589f8Merge pull request #343 from chetant/mvn_mingw32Edwin Brady fc5bd4aneed to update mvn during build as wellChetan Taralekar e18c3efFixed mvn for mingw32Chetan Taralekar f885274Fix ordering of auto-implicits with 'using' 'using' arguments always now appear before fully implicit arguments, rather than the order we happen to find them in. TODO: Better would be to sort according to which ones we know depend on each other...Edwin Brady 894db6fMerge pull request #340 from JanBessai/BackendTargetSpecificationEdwin Brady 02f57efMerge pull request #339 from david-christiansen/gitignoreEdwin Brady 46964d7Merge pull request #338 from david-christiansen/provider-tutorialEdwin Brady 41ca744Merge pull request #316 from bitlisp/default-bignumsEdwin Brady d6169acFix tutorial textJan Bessai eacfe5cAdded backend target specification to %lib, %link and %include directivesJan Bessai 9159848Add tutorial LaTeX by-products to .gitignoreDavid Christiansen 63c90dbAdded type providers to tutorialDavid Christiansen ee77b14Fix typo: "foriegn" -> "foreign"David Christiansen 2fab1b2More Integer fixupsBenjamin Saunders ca9fce6Fix for proofs in test025 (until I've added support for Decidable.Order)Jan Bessai f2f0e07Default to Integer instead of Int, and adjust fromInteger accordinglyBenjamin Saunders b915635Merge pull request #335 from david-christiansen/providers-workEdwin Brady 06a7456Merge pull request #334 from JanBessai/masterEdwin Brady b906162Make test026 more robustDavid Christiansen f148775Make prim__readString more consistent with C codeDavid Christiansen 2544d93Strictly evaluate type constructor argsDavid Christiansen ed0ba83Strictly evaluate data constructor argsDavid Christiansen 9054e62Fix wrong result type for idris_peek in JavaJan Bessai