|Maintainer||Simon Meier <email@example.com>|
Big-step proofs using case distinctions on the possible sources of a fact.
- unsolvedChainConstraints :: CaseDistinction -> [Int]
- precomputeCaseDistinctions :: ProofContext -> [LNGuarded] -> [CaseDistinction]
- refineWithTypingAsms :: [LNGuarded] -> ProofContext -> [CaseDistinction] -> [CaseDistinction]
- solveWithCaseDistinction :: ProofContext -> [CaseDistinction] -> Goal -> Maybe (Reduction [String])
- removeRedundantCases :: ProofContext -> [LVar] -> (a -> System) -> [a] -> [a]
Precomputed case distinctions
The number of remaining chain constraints of each case.
Precompute a saturated set of case distinctions.
Typing assumptions to use.
Proof context to use.
Original, untyped case distinctions.
Refined, typed case distinctions.
Refine a set of case distinction by exploiting additional typing assumptions.
Try to solve a premise goal or
KU action using the first precomputed
case distinction with a matching premise.
Given a list of stable variables (that are referenced from outside and cannot be simply renamed) and a list containing systems, this function returns a subsequence of the list such that for all removed systems, there is a remaining system that is equal modulo renaming of non-stable variables.