git.iko.soy/Idris-dev
on bf4e535 help sign in
history ofsrc/Idris/IBC.hs
all commits
13a36a3Annotate functions as %hint for auto searchEdwin Brady 95eee3cRemove no longer used primitives from TTEdwin Brady fc02362Support externally defined primitivesEdwin Brady d57d60aUse a Set for universe constraintsEdwin Brady 15737d9Trickiness with implicits in dependent classesEdwin Brady 147149bAdd 'determining parameters' for classesEdwin Brady 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 f7648dbForeign export lists in IOEdwin Brady 9249aaeIBC generation pattern match completenessDavid Raymond Christiansen 13e8ad8Plumb source locations through Tactical's elabDavid Raymond Christiansen a0346b6Begin implementation of reflected elab monadDavid Raymond Christiansen 40d094dExpose equality proofs in with ruleEdwin Brady 26cfbe9Scoped implicits fixEdwin Brady e13e48dMerge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady 8096500Add %used pragmaEdwin Brady 27e4266Add IDRIS_LIBRARY_PATH environment variableBrian McKenna d5377beNew language-dependent FFIEdwin Brady e0cab49Allow implicits to appear anywhereEdwin Brady 17fe233Add scoped implicit argument to PiEdwin Brady 0a1b72cMerge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady cad3b02Eat less memory by sharing namesEdwin Brady 6b803b7Allow documentation for modulesDavid Raymond Christiansen 2ec25c2Do more forcing in IBCEdwin Brady 7c34217Allow class constraints to be namedEdwin Brady 02a36adAllow :search and :apropos to search packagesEdwin Brady 26da5c7Save index file when installing a packageEdwin Brady 91cd4d5Better message on IBC load failureEdwin Brady e95c877Make pattern matching consistent in lambda/letEdwin Brady ec7a6a7Fix doc buildEdwin Brady 7b5f4aaFix visibility of imported thingsEdwin Brady e34c6dfAdd proper namespace to class instancesEdwin Brady 2c39286Fix for name clashes when applying transformationsEdwin Brady f1e161dA new primitive tactic for getting source locationsDavid Raymond Christiansen 4130476Just store sorted list of syntax rulesAlexander Shabalin 9d804b5Optimize custom syntax rulesAlexander Shabalin e90316aSupport type errors in docstringsDavid Raymond Christiansen 56c216dIncrement IBCEdwin Brady edb9980Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match upAhmad Salim Al-Sibahi 869e6caMerge branch 'master' of git://github.com/idris-lang/Idris-dev into partial-evalEdwin Brady 37748ceAdd transformation rules for partial evaluationEdwin Brady 7383b1cSupport nested quasiquotationDavid Raymond Christiansen 37292e1Save terms in docstringsDavid Raymond Christiansen 323a109Use exact name lookup when building from ibcEdwin Brady 7e7368dStore kind in Pi bindersEdwin Brady 218c735Mark 'case' on unique types as updatableEdwin Brady 9abbc3fCache uniqueness information in NameTypeEdwin Brady 9ceece1EXPERIMENTAL uniqueness typesEdwin Brady ddced5cStore parameters in function typesEdwin Brady