git.iko.soy/Idris-dev
on 385dcbf help sign in
history ofsrc/Idris/Core/TT.hs
all commits
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 eb99603Some renaming, for better display of docs/holesEdwin 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 b774d12Remove NLet binder from reflection APIDavid Raymond Christiansen 105c230Simplify reflection and RawDavid Raymond Christiansen 1cdc9ddReduce space leak through ugly DeepSeq hackDavid Raymond Christiansen c931effProof search improvementsEdwin Brady ab63941Added top-level %runElab supportDavid Raymond Christiansen 7095d6cProof search should only use user visible namesEdwin Brady