git.iko.soy/Idris-dev
on 13ebfcf help sign in
history ofsrc/Idris/DeepSeq.hs
all commits
6fe15eaAllow type providers to have docstringsAdam Sandberg Eriksson 7ba4da0Instance docs: instance parameter documentationAdam Sandberg Eriksson 2d205a6Instance docs: basic plumbing of types and parsingAdam Sandberg Eriksson 13e8ad8Plumb source locations through Tactical's elabDavid Raymond Christiansen a0346b6Begin implementation of reflected elab monadDavid Raymond Christiansen f17606a"claim" and "unfocus" tacticsDavid Raymond Christiansen 40d094dExpose equality proofs in with ruleEdwin Brady 26cfbe9Scoped implicits fixEdwin Brady e0cab49Allow implicits to appear anywhereEdwin Brady 177b96bRemove -Werror from all filesDavid Raymond Christiansen 2ec25c2Do more forcing in IBCEdwin Brady e95c877Make pattern matching consistent in lambda/letEdwin Brady f1e161dA new primitive tactic for getting source locationsDavid Raymond Christiansen edb9980Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match upAhmad Salim Al-Sibahi 37292e1Save terms in docstringsDavid Raymond Christiansen 9ceece1EXPERIMENTAL uniqueness typesEdwin Brady 84b172aAdd tactics "skip" and "fail"David Raymond Christiansen 1269791Keep type arguments of = when unelaboratingEdwin Brady c90d4b4Parsing for quasiquotesDavid Raymond Christiansen 4833cb3Merge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/casetacticAhmad Salim Al-Sibahi 9993f3bAdd pi to overridable syntax in DSL blocksDavid Raymond Christiansen e91819cFinal cleanup/check of case tactic implementationAhmad Salim Al-Sibahi e5bc47eDistinguish postulate providers and type providers at use siteDavid Raymond Christiansen 5c4ee75Make load to line work with mutual blocksEdwin Brady 7e78f0aExtend positivity check for mutual data typesEdwin Brady 602552eAdd :loadto commandEdwin Brady 094be98Add an optional depth to 'search' tacticEdwin Brady 719d472'search' now fails if there are metavariablesEdwin Brady 4035b5dAdd a field for parameter docstrings in the PClass constructor of PDecl'Paul Koerbitz 78ff448Bug fixing of induction bugsAhmad Salim Al-Sibahi e07c13dAdd :refine (:ref) command for refining a holeEdwin Brady eedf489Remove collapsibility and forceability altogether.Matus Tejiscak 5b62302Add "detaggable" as an argument to OptInfo.Matus Tejiscak 9b80d0dAdd an "inaccessible" field to OptData.Matus Tejiscak d3eb486First attempt now at substitution to default argsTimo Petteri Sinnemäki a7e6550Merge pull request #962 from david-christiansen/markdown-docsEdwin Brady d910c2cUse Markdown to represent docstringsDavid Raymond Christiansen 8f93b00Syntax for failures in pattern matching let/<-Edwin Brady c1ef938New syntax for documentation commentsDavid Raymond Christiansen bd744f1Propagate function name to tacticsEdwin Brady 0875310Control whether provider decls accept postulatesDavid Raymond Christiansen f6bebd3Proper pretty-printing of dependent pairsDavid Raymond Christiansen e80f871Annotate and colour pairs and () properlyDavid Raymond Christiansen fe3f03fAdded %error_reverse annotationEdwin Brady 803194fArgument options (instead of just a Bool for lazy)Edwin Brady 66ec833Minor memory usage improvementsEdwin Brady 4e6adebSeparate Core NFData instancesEdwin Brady 67da31aMerge branch 'master' into cabal-libraryBrian McKenna dccddd2Merge branch 'forceability-cleanup-squashed' of https://github.com/ziman/idris into ziman-forceability-cleanup-squashedEdwin Brady 2e570a3Merge branch 'default-superclass-instances' of https://github.com/puffnfresh/Idris-dev into puffnfresh-default-superclass-instancesEdwin Brady