on 8935fed help sign in
all commits
c3def79Rename Tactical to ElabDavid Raymond Christiansen 6c4553cMake --quiet imply non-verbosityDavid Raymond Christiansen 13a36a3Annotate functions as %hint for auto searchEdwin Brady fc02362Support externally defined primitivesEdwin Brady d57d60aUse a Set for universe constraintsEdwin Brady 22d1ae6Propagation of explicit arguments in typeclassesEdwin Brady 174395bMerge remote-tracking branch 'upstream/master' into issue2004Andreas Reuleaux 15737d9Trickiness with implicits in dependent classesEdwin Brady b989e36dead code: renderWidth nowhere usedAndreas Reuleaux 361efb5Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 147149bAdd 'determining parameters' for classesEdwin Brady c2dc6ecAllow new-style tactics to declare function signaturesDavid Raymond Christiansen 426d052Add provenance flag to unification errorsEdwin Brady 7ba4da0Instance docs: instance parameter documentationAdam Sandberg Eriksson 2d205a6Instance docs: basic plumbing of types and parsingAdam Sandberg Eriksson 20e1debFix irrelevance bugEdwin Brady f7648dbForeign export lists in IOEdwin Brady 41711c7stripLinear needs to check dependent pairsEdwin Brady 8697358Fix scope error when shadowingEdwin Brady 13e8ad8Plumb source locations through Tactical's elabDavid Raymond Christiansen a0346b6Begin implementation of reflected elab monadDavid Raymond Christiansen 40d094dExpose equality proofs in with ruleEdwin Brady b85b2ebRename ideslave to ide-modeDavid Raymond Christiansen ef954e1Fix the new totality testDavid Raymond Christiansen 8096500Add %used pragmaEdwin Brady 60e4921Relax lower bound on mtlEric Mertens c729d2fSupport scoped type class constraintsEdwin Brady e0cab49Allow implicits to appear anywhereEdwin Brady 17fe233Add scoped implicit argument to PiEdwin Brady cad3b02Eat less memory by sharing namesEdwin Brady 2ec25c2Do more forcing in IBCEdwin Brady 7c34217Allow class constraints to be namedEdwin Brady ee32989Search in current elaboration stack for instancesEdwin Brady 2e6b5e0Fix universe checking errorEdwin Brady e95c877Make pattern matching consistent in lambda/letEdwin Brady 4175a7fCoverage checker should ignore hidden argumentsEdwin Brady 8789717Hide other unmatchable patternsEdwin Brady 0d8a153New way of dealing with unmatchable patternsEdwin Brady 684a578Completely replace ErrorT with ExceptTbmsherman 7b5f4aaFix visibility of imported thingsEdwin Brady fbcd643Check datatypes are not redefinedEdwin Brady 73e9c30Lifted TODO/FIXME from Idris/AbsSyntax.hsJan de Muijnck-Hughes f866fecUse Set for unique name checking for efficiencyEdwin Brady cdff1dbMerge pull request #1659 from edwinb/partial-evalEdwin Brady 8e6b636Optimisation optionsEdwin Brady 03f6913Partially evaluate type class dictionariesEdwin Brady e90316aSupport type errors in docstringsDavid Raymond Christiansen 6f9d433Parameters should be made 'static'Edwin Brady e890280Merge pull request #1619 from ahmadsalim/feature/renamevoidEdwin Brady 6e74e33Fix for pattern vars in transformsEdwin Brady