git.iko.soy/Idris-dev
on bf4e535 help sign in
history ofsrc/Idris/ElabDecls.hs
all commits
fc02362Support externally defined primitivesEdwin 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 c729d2fSupport scoped type class constraintsEdwin Brady 17fe233Add scoped implicit argument to PiEdwin Brady f1e161dA new primitive tactic for getting source locationsDavid Raymond Christiansen e90316aSupport type errors in docstringsDavid Raymond Christiansen e890280Merge pull request #1619 from ahmadsalim/feature/renamevoidEdwin Brady 3ade599Partial evaluator fixesEdwin Brady edb9980Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match upAhmad Salim Al-Sibahi 37748ceAdd transformation rules for partial evaluationEdwin Brady 6faa1abRenaming of built-in datatypes works finallyAhmad Salim Al-Sibahi f0ed9e9First renaming attemptAhmad Salim Al-Sibahi c55895dFix universe errors, update testsEdwin Brady 7e7368dStore kind in Pi bindersEdwin Brady 9abbc3fCache uniqueness information in NameTypeEdwin Brady c6574b4Added idris-c executableEdwin Brady c72d0f4Split elaborator into multiple source filesEdwin Brady 816e85bReinsert check for constructor/family mismatch.David Raymond Christiansen 84b172aAdd tactics "skip" and "fail"David Raymond Christiansen 734a7bfGenerate better record projection typesEdwin Brady 6e39ba5Normalise everything before 'with' abstractionEdwin Brady 1d23ad1Normalise before abstracting over 'with' typeEdwin Brady c1968edFix parameter spotting in function typesEdwin Brady 1cdd0dfDon't do trace when `with` doesn't matchDavid Raymond Christiansen e6bec02Fix parameter propagation on CAFsEdwin Brady e363c09Better treatment of unbound implicitsEdwin Brady d9513aaMerge pull request #1360 from ziman/case-elab-erasureEdwin Brady 60b1f18Added some additional documentation for partial evaluationAhmad Salim Al-Sibahi c201192Bring erasure info to the case tree builder.Matus Tejiscak 67f7373Support builds that doesn't use cabal for libs and rtsniklas 80d1a88Fix implicit spotting in case blocksEdwin Brady 4833cb3Merge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/casetacticAhmad Salim Al-Sibahi 5045daeAdded tactic for case analysis. Also, induction now work on expressions instead of simply names.Ahmad Salim Al-Sibahi e5bc47eDistinguish postulate providers and type providers at use siteDavid Raymond Christiansen 21124c3Merge remote-tracking branch 'upstream/master' into cantResolveAltsbmsherman 9907240Add new Err constructor to disambiguate the CantResolveAlts constructor.bmsherman 7e78f0aExtend positivity check for mutual data typesEdwin Brady 636e6e1Fix for repeated variables in instance headEdwin Brady 175a735Make sure binders are unique before case treeEdwin Brady 8215c60Fix zero argument with clausesEdwin Brady f53580aChange type class top level method generationEdwin Brady f02f3c0Check if class is meant to be empty...Edwin Brady f8e6549:addclause now adds template bodies to instancesEdwin Brady af99a9dAdd :makelemma command in interactive editingEdwin Brady 3825ad8Remove spurious error from 'setter' warningEdwin Brady 0c1bc8dPropagate bound implicits to record updatesEdwin Brady 5e3c248Change impl argument to a pretty printing opt recordPeter Minten