git.iko.soy/Idris-dev
on 1b71663 help sign in
history ofsrc/Idris/Core/TT.hs
all commits
193589fWhy nub a list when you can use a set.Jan de Muijnck-Hughes fb717ccFix compilation with GHC 8.4Niklas Larsson cc7ef9aRemove old eliminator generation and induction tactic (#4351)Ahmad Salim Al-Sibahi 5813103Fix for stylishEdwin Brady db69077Fix binding rules in patternsEdwin Brady b1a4264Improve error message locations (#4210)Jason Felice 3ccb494Remove the empty property 'copyright'.Jan de Muijnck-Hughes aad7688Megaparsec prep (#4164)Jason Felice 4f1f462Fix LaTeX pretty printing of backslash, braces and percentJoomy Korkut 4a3fe0cLinearTypes extension improvementsEdwin Brady 83bb62fUnused binds (#4067)Jason Felice d4bd8e6Clean up unused imports (#4065)Jason Felice 5d7388bMove extensions into source filesEdwin Brady 3e4752fFix name decorationEdwin Brady 024663cMerge pull request #3475 from enolan/stylish-travisEdwin Brady fb185aaCheck for linearity of constructorsEdwin Brady a5033e7Add linear LamEdwin Brady 1e3651fCheck multiplicities on RigCountsEdwin Brady e1c210bAdd 'RigCount' to Pi and PVarEdwin Brady e3daf28Add RigCount to environmentEdwin Brady ea88b5eBetter choice of pattern to inspect in coverageEdwin Brady 8ea27aeRemove a needless 'nub'Edwin Brady 7ac40afStylish changes since this PR was originally submittedEcho Nolan 3fc435fTurn on some LANGUAGE pragmas to make stylish-haskell happy.Echo Nolan f467346Detect implicit parameters to interfacesEdwin Brady e6ceb5cAlphabetize and indent imports and LANGUAGE pragmasEcho Nolan 0df1270Change Instance to implementation (#3404)(λ _ λ) 289df05Merge pull request #3376 from zjhmale/fix-error-messageAhmad Salim Al-Sibahi 4615cffMerge pull request #3399 from enolan/hot-commentsAhmad Salim Al-Sibahi 53fae80use interface in error message when check instancezjhmale 06d9db6Use interface instead class or type class in documentations (#3379)(λ _ λ) 9c636f4Remove a bunch of "deriving instance NFData" hot commentsEcho Nolan 29046ccPrint core definitionsDavid Christiansen 9baa5ceUse GHC generics for NFData instancesEcho Nolan fc3e88cMerge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady fdfa04cStore file with constraints + exportEdwin Brady da1d168Merge pull request #3202 from ahmadsalim/feature/betterrewritingerrorAhmad Salim Al-Sibahi be093dcAdded more context to the no rewriting error, to include terms being rewritten withAhmad Salim Al-Sibahi c2446faMerge pull request #3196 from Melvar/instate-parentnEdwin Brady c70672dFix ordering of dependent patterns/implicitsEdwin Brady c6f1061Remove vestiges of pre-SpecialName namesMelvar Chen 76d57f2Alpha conversion in substTermEdwin Brady 0896073Added documentation for modules.Jan de Muijnck-Hughes fe1d470Totality checking now looks inside case directlyEdwin Brady 7e7d0ebElaboration of local applicationsEdwin Brady 4079f54Use bit-pattern identity for DoubleDavid Christiansen c9d2027Use exact name lookup for hidingEdwin Brady 1cf8fe9Context for "Can't find implementation"Edwin Brady f7a9c28Tweak implicit name rulesEdwin Brady e97f02aFix instance->implementation in displayEdwin Brady