git.iko.soy/Idris-dev
on bf4e535 help sign in
history ofsrc/Idris/Core/TT.hs
all commits
187730aAdd missing clause in showCGSam Elliott 95eee3cRemove no longer used primitives from TTEdwin Brady 8472966Remove Buffer/BitVectors from compiler/C rtsEdwin Brady 2d503f1Fix interactive proverEdwin Brady d57d60aUse a Set for universe constraintsEdwin Brady dbe0a3cCheck class arguments for injectivityEdwin Brady f4aaf01Guard !! in forgetEnvEdwin Brady 2a70296Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen c2dc6ecAllow new-style tactics to declare function signaturesDavid Raymond Christiansen c66df51Propagate unification solutions into types on 'P'Edwin Brady be9ffc9Proper error message for missing eliminatorsEdwin Brady 5ce7362Type class resolution fixEdwin Brady 6d768bbMore information if a function is overappliedEdwin Brady 01c4f2aA bit more unification error provenanceEdwin Brady 75f6c2dAdd :core to the REPLDavid Raymond Christiansen bb013f0Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 3d87454TT pretty-printing - also in elab debugDavid Raymond Christiansen 179c704Record provenance of types in 'fill' errorsEdwin Brady 426d052Add provenance flag to unification errorsEdwin Brady 02d0078Add beginning of elaborator debugging errorsDavid Raymond Christiansen 26cfbe9Scoped implicits fixEdwin Brady 9150698Primitive type for world stateEdwin Brady 2fd3ebcderive Data and Typeable for ImplicitInfoEdwin Brady 02d26ecMerge pull request #1841 from david-christiansen/issue/1806David Christiansen bf2f3ccAdd a default case to uniqueNameFromDavid Raymond Christiansen c729d2fSupport scoped type class constraintsEdwin Brady 0b23ef2Replace _ patterns with fresh variables under @-patternsDavid Raymond Christiansen 17fe233Add scoped implicit argument to PiEdwin Brady 2ec25c2Do more forcing in IBCEdwin Brady 8628481refsIn should take all the PsEdwin Brady d40cd6fCheck for duplicate names in Can't ConvertEdwin Brady 0d8a153New way of dealing with unmatchable patternsEdwin Brady 6d54cb3Disallow explicit types on LHSEdwin Brady 00f1cd5Use ExceptT instead of ErrorTbmsherman e34c6dfAdd proper namespace to class instancesEdwin Brady bcd2db1Check target of 'with' is a value (not a function)Edwin Brady b0a0c0cImprovement for 'auto'Edwin Brady 4547329Lifted TODO from Core/Tt.Jan de Muijnck-Hughes f866fecUse Set for unique name checking for efficiencyEdwin Brady e90316aSupport type errors in docstringsDavid Raymond Christiansen 7ce4d90Add annotations for :search result classificationbmsherman 971d88dAnnotate several top-level functionsMichael Maloney 486c4c0Add missing pattern in TT.hsMichael Weiss 7e7368dStore kind in Pi bindersEdwin Brady bc2bcb6Add Borrowed typesEdwin Brady e30ff97Merge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady a1fb7a3Inline with blocksEdwin Brady 2aaff41Stop erasing binder types in executorDavid Raymond Christiansen 9abbc3fCache uniqueness information in NameTypeEdwin Brady 41e9032Check constructor kinds for uniqueness errorsEdwin Brady