Instances For
Instances For
Instances For
Instances For
Instances For
Try to close goal using rfl with smart unfolding turned off.
Instances For
Eliminate namedPatterns from equation, and trivial hypotheses.
Instances For
Instances For
Some of the hypotheses added by mkEqnTypes may not be used by the actual proof (i.e., value argument).
This method eliminates them.
Alternative solution: improve saveEqn and make sure it never includes unnecessary hypotheses.
These hypotheses are leftovers from tactics such as splitMatch? used in mkEqnTypes.
Instances For
Instances For
Delta reduce the equation left-hand-side
Instances For
Instances For
Apply whnfR to lhs, return none if lhs was not modified
Instances For
- map : Lean.PHashMap Lake.Name Lake.Name
Instances For
Auxiliary method for mkUnfoldEq. The structure is based on mkEqnTypes.
mvarId is the goal to be proved. It is a goal of the form
declName x_1 ... x_n = body[x_1, ..., x_n]
The proof is constracted using the automatically generated equational theorems.
We basically keep splitting the match and if-then-else expressions in the right hand side
until one of the equational theorems is applicable.
Instances For
Generate the "unfold" lemma for declName.