git.iko.soy/Idris-dev
on 1b71663 help sign in
history ofsrc/Idris/Core/Binary.hs
all commits
cc7ef9aRemove old eliminator generation and induction tactic (#4351)Ahmad Salim Al-Sibahi 3ccb494Remove the empty property 'copyright'.Jan de Muijnck-Hughes 391c93cUse default Binary implementation here, tooJason Felice d4bd8e6Clean up unused imports (#4065)Jason Felice ab65a30Merge branch 'master' of Idris-dev into issue3796Edmund Smith 5d7388bMove extensions into source filesEdwin Brady 59bfe8bUse explicit IEEE-friendly marshallingEdmund Smith a5033e7Add linear LamEdwin Brady e1c210bAdd 'RigCount' to Pi and PVarEdwin Brady ea88b5eBetter choice of pattern to inspect in coverageEdwin Brady e6ceb5cAlphabetize and indent imports and LANGUAGE pragmasEcho Nolan 0df1270Change Instance to implementation (#3404)(λ _ λ) fc3e88cMerge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady fdfa04cStore file with constraints + exportEdwin Brady be093dcAdded more context to the no rewriting error, to include terms being rewritten withAhmad Salim Al-Sibahi c70672dFix ordering of dependent patterns/implicitsEdwin Brady 0896073Added documentation for modules.Jan de Muijnck-Hughes 1cf8fe9Context for "Can't find implementation"Edwin Brady 06edf43Add implicit lambdas for top level implicitsEdwin Brady 83f0af1Display expected type of RHS in error messagesEdwin Brady 83ca4aeFriendlier error on proof search failureDavid Raymond Christiansen 0f89577Remove NErasedDavid Raymond Christiansen d5b66a9Show source location of case block namesDavid Raymond Christiansen 32ce95fBetter error on staging problem for Elab scriptsDavid Raymond Christiansen 105c230Simplify reflection and RawDavid Raymond Christiansen ab63941Added top-level %runElab supportDavid Raymond Christiansen 7095d6cProof search should only use user visible namesEdwin Brady 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