Equations
- Lean.Elab.Eqns.splitMatch? mvarId declNames = Lean.commitWhenSome? do let target ← mvarId.getType' Lean.Elab.Eqns.splitMatch?.go mvarId declNames target ∅
Instances For
Eliminate namedPatterns
from equation, and trivial hypotheses.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Delta reduce the equation left-hand-side
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.Eqns.tryContradiction mvarId = mvarId.contradictionCore { useDecide := true, emptyType := true, searchFuel := 16, genDiseq := true }
Instances For
Generate equations for declName
.
This unfolds the function application on the LHS (using an unfold theorem, if present, or else by
delta-reduction), calculates the types for the equational theorems using mkEqnTypes
, and then
proves them using mkEqnProof
.
This is currently used for non-recursive functions and for functions defined by partial_fixpoint.
Equations
- One or more equations did not get rendered due to their size.
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 constructed 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Generate the "unfold" lemma for declName
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.Eqns.getUnfoldFor? declName getInfo? = match getInfo? () with | some info => do let __do_lift ← Lean.Elab.Eqns.mkUnfoldEq declName info pure (some __do_lift) | x => pure none