git.iko.soy/Idris-dev
on 1b71663 help sign in
history ofsrc/Idris/Core/ProofState.hs
all commits
fb717ccFix compilation with GHC 8.4Niklas Larsson cc7ef9aRemove old eliminator generation and induction tactic (#4351)Ahmad Salim Al-Sibahi 06db7dcFix corner case with dot patternsEdwin Brady 3ccb494Remove the empty property 'copyright'.Jan de Muijnck-Hughes dd5b4d7Fixed unused imports reported by ghcMerlin Göttlinger 4a3fe0cLinearTypes extension improvementsEdwin Brady 83bb62fUnused binds (#4067)Jason Felice d4bd8e6Clean up unused imports (#4065)Jason Felice 5d7388bMove extensions into source filesEdwin Brady 9e69858Fixed unstylized things in Idris and stylize.sh scriptAhmad Salim Al-Sibahi a5033e7Add linear LamEdwin Brady 2f3c9a5Add RigCount to pattern bindingsEdwin Brady 491633bSyntax for linear argumentsEdwin Brady e1c210bAdd 'RigCount' to Pi and PVarEdwin Brady e3daf28Add RigCount to environmentEdwin Brady b79bf7bFix for cyclic solutions in unifyProblemsEdwin Brady b0130d6Add whnfArgsEdwin Brady b28f12bWHNF takes an environmentEdwin Brady 7537cc4Change totality checking and inliningEdwin Brady e6ceb5cAlphabetize and indent imports and LANGUAGE pragmasEcho Nolan 0df1270Change Instance to implementation (#3404)(λ _ λ) 06d9db6Use interface instead class or type class in documentations (#3379)(λ _ λ) 728adb7Fix a unification bugEdwin Brady 08cef17HLint DIrected Code CleanupJan de Muijnck-Hughes fdfa04cStore file with constraints + exportEdwin Brady 83ef000Check delayed holes are still holesEdwin Brady 0896073Added documentation for modules.Jan de Muijnck-Hughes eaf5211Add the ability to define datatypes in ElabDavid Raymond Christiansen 310f046Fix case split/unification bugEdwin Brady 3d2fa6cBetter elaboration of applicationsEdwin Brady 83f0af1Display expected type of RHS in error messagesEdwin Brady d5b66a9Show source location of case block namesDavid Raymond Christiansen 3b9206bError message instead of crash when searching on a guessDavid Raymond Christiansen ce403f6Merge remote-tracking branch 'upstream/master' into wip/tacticalDavid Raymond Christiansen 0497655Properly compute default lambda var namesDavid Raymond Christiansen 93dafdeMake sure deferred names are uniqueEdwin Brady c931effProof search improvementsEdwin Brady b1ce3cbImplement a form of pattern unificationEdwin Brady b573bf0Improve addImpl under PHiddenEdwin Brady 2e170bfRemove dubious matching ruleEdwin Brady 7bde028Use subst for intro, rather than updsubstDavid Raymond Christiansen 7095d6cProof search should only use user visible namesEdwin Brady 0e7c076Normalise types before detecting parametric argsEdwin Brady 01c911eFix missing case in `casetac`Brian Koropoff 268459cFailing 'focus' should be harmlessEdwin Brady 3034fb6Remove argument ordering hack in elaboratorEdwin Brady d97715ePlumb datatype information through the proof stateDavid Raymond Christiansen 8ab2814Mark 'complete' terms to save time in elaborationEdwin Brady f987aecAdd info field to AppEdwin Brady 147149bAdd 'determining parameters' for classesEdwin Brady