Eliminates arguments for named parameters and the associated equation proofs.
Equality parameters associated with the
h : discrnotation are replaced with
rflproofs. Recall that this kind of parameter always occurs after the parameters correspoting to pattern variables.
numNonEqParamsis the size of the prefix.
k takes four arguments
ys args mask type.
ysare variables for the hypotheses that have not been eliminated.
eqsare variables for equality hypotheses associated with discriminants annotated with
h : discr.
argsare the arguments for the alternative
altthat has type
ys.size <= args.size
mask[i]is true if the hypotheses has not been eliminated.
mask.size == args.size.
typeis the resulting type for
We use the
mask to build the splitter proof. See
- mvarId : Lean.MVarId
State for the equational theorem hypothesis simplifier.
Recall that each equation contains additional hypotheses to ensure the associated case does not taken by previous cases. We have one hypothesis for each previous case.
We use tactics to minimize code duplication.
Auxiliary tactic that tries to replace as many variables as possible and then apply
We use it to discard redundant hypotheses.