git.iko.soy/Idris-dev
on 239c8ca help sign in
history ofsrc/Idris/Core/ProofState.hs
all commits
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 c66df51Propagate unification solutions into types on 'P'Edwin Brady be9ffc9Proper error message for missing eliminatorsEdwin Brady 6d768bbMore information if a function is overappliedEdwin Brady 01c4f2aA bit more unification error provenanceEdwin Brady 179c704Record provenance of types in 'fill' errorsEdwin Brady 426d052Add provenance flag to unification errorsEdwin Brady f17606a"claim" and "unfocus" tacticsDavid Raymond Christiansen 26cfbe9Scoped implicits fixEdwin Brady cb005bcFix overenthusiastic unificationEdwin Brady 39e4eb0IO primitives tweak to support JSEdwin Brady 72aa6b9Proper error when merging solutions failsEdwin Brady c729d2fSupport scoped type class constraintsEdwin Brady e0cab49Allow implicits to appear anywhereEdwin Brady 17fe233Add scoped implicit argument to PiEdwin Brady 0d8a153New way of dealing with unmatchable patternsEdwin Brady ba51147Removing matching on PSEdwin Brady 6d54cb3Disallow explicit types on LHSEdwin Brady 6b6aae0Avoid retrying unification problems constantlyEdwin Brady b0a0c0cImprovement for 'auto'Edwin Brady 127db00Lifted a FIXME from Core/ProofStateJan de Muijnck-Hughes 9fd9de7Proper error for missing eliminatorEdwin Brady 3ade599Partial evaluator fixesEdwin Brady 971d88dAnnotate several top-level functionsMichael Maloney 7e7368dStore kind in Pi bindersEdwin Brady 9ceece1EXPERIMENTAL uniqueness typesEdwin Brady ab36099Use a zipper-like proof stateEdwin Brady a9dd2e4Lift out proof term into a separate moduleEdwin Brady e6e1ad9Unification fixEdwin Brady 0a1965eChange 'Not a guess' errorEdwin Brady 8ed343bRemove dodgy unification hackEdwin Brady e363c09Better treatment of unbound implicitsEdwin Brady 4833cb3Merge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/casetacticAhmad Salim Al-Sibahi 5045daeAdded tactic for case analysis. Also, induction now work on expressions instead of simply names.Ahmad Salim Al-Sibahi a0b05e2Allow induction on terms instead of simply namesAhmad Salim Al-Sibahi 921b766Fix name propagation in error messagesEdwin Brady 41f921fUnify more things!Edwin Brady d10c1e9Can't assume explicit names in updateSolvedEdwin Brady 5a5eecaMerge pull request #1143 from ahmadsalim/bug/inductionfixDavid Christiansen e36c883Fix #1015raichoo 78ff448Bug fixing of induction bugsAhmad Salim Al-Sibahi 62705e4Tweak mergeNotunifiedEdwin Brady