Documentation

Lean.Elab.PreDefinition.Eqns

Instances For
Equations
partial def Lean.Elab.Eqns.expand (progress : Bool) (e : Expr) :

Zeta reduces let and let_fun while consuming metadata. Returns true if progress is made.

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

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 : Array Name) (mvarId : MVarId) :
Equations

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 declValue type value : Expr) (xs : Array Expr) (lctx : 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 : MVarId) (declName : 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
def Lean.Elab.Eqns.mkEqns (declName : Name) (declNames : Array Name) (tryRefl : Bool := true) :

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, well-founded recursion and partial_fixpoint, but not for structural recursion.

Equations
  • One or more equations did not get rendered due to their size.
def Lean.Elab.Eqns.mkUnfoldProof (declName : Name) (mvarId : 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 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.
partial def Lean.Elab.Eqns.mkUnfoldProof.go (declName : Name) (tryEqns : MVarIdMetaM Bool) (mvarId : MVarId) :

Generate the "unfold" lemma for declName.

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