# Documentation

Lean.Elab.PreDefinition.Eqns

Instances For
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
def Lean.Elab.Eqns.splitMatch? (mvarId : Lean.MVarId) (declNames : ) :
Equations
partial def Lean.Elab.Eqns.splitMatch?.go (mvarId : Lean.MVarId) (declNames : ) (target : Lean.Expr) (badCases : Lean.ExprSet) :
• declNames :
Instances For

Try to close goal using rfl with smart unfolding turned off.

Equations
• One or more equations did not get rendered due to their size.

Eliminate namedPatterns from equation, and trivial hypotheses.

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Eqns.mkEqnTypes (declNames : ) (mvarId : Lean.MVarId) :
Equations
• One or more equations did not get rendered due to their size.
partial def Lean.Elab.Eqns.mkEqnTypes.go (declNames : ) (mvarId : Lean.MVarId) :

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.
def Lean.Elab.Eqns.removeUnusedEqnHypotheses.go (declType : Lean.Expr) (declValue : Lean.Expr) (type : Lean.Expr) (value : Lean.Expr) (xs : ) (lctx : Lean.LocalContext) :

Delta reduce the equation left-hand-side

Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Eqns.deltaRHS? (mvarId : Lean.MVarId) (declName : Lean.Name) :
Equations
• One or more equations did not get rendered due to their size.

Apply whnfR to lhs, return none if lhs was not modified

Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
def Lean.Elab.Eqns.mkUnfoldProof (declName : Lean.Name) (mvarId : Lean.MVarId) :

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.

Equations
• One or more equations did not get rendered due to their size.
partial def Lean.Elab.Eqns.mkUnfoldProof.go (declName : Lean.Name) (tryEqns : ) (mvarId : Lean.MVarId) :

Generate the "unfold" lemma for declName.

Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Eqns.getUnfoldFor? (declName : Lean.Name) (getInfo? : ) :
Equations
• One or more equations did not get rendered due to their size.