structure Lean.Elab.Eqns.EqnInfoCore : Type

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

def Lean.Elab.Eqns.instInhabitedEqnInfoCore.default : EqnInfoCore

Equations

• Lean.Elab.Eqns.instInhabitedEqnInfoCore.default = { declName := default, levelParams := default, type := default, value := default }

instance Lean.Elab.Eqns.instInhabitedEqnInfoCore : Inhabited EqnInfoCore

Equations

• Lean.Elab.Eqns.instInhabitedEqnInfoCore = { default := Lean.Elab.Eqns.instInhabitedEqnInfoCore.default }

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)

Equations

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

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

Equations

• Lean.Elab.Eqns.simpMatch? mvarId = do let mvarId' ← Lean.Meta.Split.simpMatchTarget mvarId if (mvarId != mvarId') = true then pure (some mvarId') else pure none

def Lean.Elab.Eqns.simpIf? (mvarId : MVarId) (useNewSemantics : Bool := false) : MetaM (Option MVarId)

Simplify if-then-expressions in the goal target. If useNewSemantics is true, the flag backward.split is ignored.

Equations

• Lean.Elab.Eqns.simpIf? mvarId useNewSemantics = do let mvarId' ← Lean.Meta.simpIfTarget mvarId true useNewSemantics if (mvarId != mvarId') = true then pure (some mvarId') else pure none

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

Equations

• Lean.Elab.Eqns.splitMatch? mvarId declNames = Lean.commitWhenSome? do let target ← mvarId.getType' Lean.Elab.Eqns.splitMatch?.go✝ mvarId declNames target ∅

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

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

Equations

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

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

Eliminate namedPatterns from equation, and trivial hypotheses.

Equations

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

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

Equations

• Lean.Elab.Eqns.mkEqnTypes declNames mvarId = do let __discr ← (Lean.Elab.Eqns.mkEqnTypes.go✝ declNames mvarId).run #[] match __discr with | (fst, eqnTypes) => pure eqnTypes

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.

Equations

• Lean.Elab.Eqns.removeUnusedEqnHypotheses declType declValue = Lean.Elab.Eqns.removeUnusedEqnHypotheses.go✝ declType declValue declType declValue #[] { }

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

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) : MetaM (Option MVarId)

Equations

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

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

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

Equations

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

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

Equations

• Lean.Elab.Eqns.tryContradiction mvarId = mvarId.contradictionCore { genDiseq := true }

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.

Equations

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

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.

Equations

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