on 54e4e41 help sign in
all commits
e1c79efBetter error when no alternative is validEdwin Brady 4ede52dAllow the pretty-printing of Raw termsDavid Raymond Christiansen 11266fbUse Text's own Binary instanceDavid Raymond Christiansen 1054d7dAdd UnknownImplicit errorEdwin Brady 518055fFully evaluate Text from BinaryNiklas Larsson c46243bInitial implementation of semantic editor hightlightingDavid Raymond Christiansen 8073344Better errors on stuck reflected elaboratorsDavid Raymond Christiansen 8ab1ac6Richer universe error objectsDavid Raymond Christiansen 3592edbReflection for SN, plus an SN for meta-stuffDavid Raymond Christiansen e17a665Convert Text to ByteStrings directlyNiklas Larsson f987aecAdd info field to AppEdwin Brady 95eee3cRemove no longer used primitives from TTEdwin Brady 8472966Remove Buffer/BitVectors from compiler/C rtsEdwin Brady d57d60aUse a Set for universe constraintsEdwin Brady 09ff7edMerge branch 'master' of https://github.com/ozgurakgun/Idris-dev into ozgurakgun-masterEdwin Brady 4a2ef38store the "involved" constraints next to the domain of a var. will help with error reporting.Ozgur Akgun dbe0a3cCheck class arguments for injectivityEdwin 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 bb013f0Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 179c704Record provenance of types in 'fill' errorsEdwin Brady 02d0078Add beginning of elaborator debugging errorsDavid Raymond Christiansen 9150698Primitive type for world stateEdwin Brady c729d2fSupport scoped type class constraintsEdwin Brady 17fe233Add scoped implicit argument to PiEdwin Brady 6b803b7Allow documentation for modulesDavid Raymond Christiansen 0d8a153New way of dealing with unmatchable patternsEdwin Brady bcd2db1Check target of 'with' is a value (not a function)Edwin Brady dd3d445Binary instance for Err + binary fixesDavid Raymond Christiansen 7e7368dStore kind in Pi bindersEdwin Brady bc2bcb6Add Borrowed typesEdwin Brady a1fb7a3Inline with blocksEdwin Brady 9abbc3fCache uniqueness information in NameTypeEdwin Brady 9ceece1EXPERIMENTAL uniqueness typesEdwin Brady d1a832aSend serialized versions of TT terms in pprintDavid Raymond Christiansen