structure Lean.Elab.Eqns.EqnInfoCore : Type

• declName : Name
• levelParams : List Name
• type : Expr
• value : Expr

instance Lean.Elab.Eqns.instInhabitedEqnInfoCore : Inhabited EqnInfoCore

partial def Lean.Elab.Eqns.expand (progress : Bool) (e : Expr) : Bool × Expr

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

def Lean.Elab.Eqns.expandRHS? (mvarId : MVarId) : MetaM (Option MVarId)

def Lean.Elab.Eqns.simpMatch? (mvarId : MVarId) : MetaM (Option MVarId)

def Lean.Elab.Eqns.simpIf? (mvarId : MVarId) : MetaM (Option MVarId)

def Lean.Elab.Eqns.splitMatch? (mvarId : MVarId) (declNames : Array Name) : MetaM (Option (List MVarId))

partial def Lean.Elab.Eqns.splitMatch?.go (mvarId : MVarId) (declNames : Array Name) (target : Expr) (badCases : ExprSet) : MetaM (Option (List MVarId))

def Lean.Elab.Eqns.tryURefl (mvarId : MVarId) : MetaM Bool

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

def Lean.Elab.Eqns.simpEqnType (eqnType : Expr) : MetaM Expr

Eliminate namedPatterns from equation, and trivial hypotheses.

def Lean.Elab.Eqns.simpEqnType.collect (e : Expr) : FVarIdSet

def Lean.Elab.Eqns.mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr)

partial def Lean.Elab.Eqns.mkEqnTypes.go (declNames : Array Name) (mvarId : MVarId) : StateRefT' IO.RealWorld (Array Expr) MetaM Unit

def Lean.Elab.Eqns.removeUnusedEqnHypotheses (declType declValue : Expr) : CoreM (Expr × Expr)

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.

def Lean.Elab.Eqns.removeUnusedEqnHypotheses.go (declType declValue type value : Expr) (xs : Array Expr) (lctx : LocalContext) : CoreM (Expr × Expr)

def Lean.Elab.Eqns.deltaLHS (mvarId : MVarId) : MetaM MVarId

Delta reduce the equation left-hand-side

def Lean.Elab.Eqns.deltaRHS? (mvarId : MVarId) (declName : Name) : MetaM (Option MVarId)

def Lean.Elab.Eqns.whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId)

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

def Lean.Elab.Eqns.tryContradiction (mvarId : MVarId) : MetaM Bool

def Lean.Elab.Eqns.mkEqns (declName : Name) (declNames : Array Name) (tryRefl : Bool := true) : MetaM (Array Name)

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.

def Lean.Elab.Eqns.mkEqns.doRealize (declName : Name) (tryRefl : Bool := true) (name : Name) (info : DefinitionVal) (type : Expr) : MetaM Unit

def Lean.Elab.Eqns.mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit

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.

partial def Lean.Elab.Eqns.mkUnfoldProof.go (declName : Name) (tryEqns : MVarId → MetaM Bool) (mvarId : MVarId) : MetaM Unit