def Lean.Meta.Match.simpH (mvarId : MVarId) (numEqs : Nat) : MetaM (Option MVarId)

Like simpH?, but works directly on a goal corresponding to the unsimplified equational theorem hypothesis, and either closes it or returns a residual goal whose type is the simplified equational theorem hypothesis.

Equations

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

def Lean.Meta.Match.simpH? (h : Expr) (numEqs : Nat) : MetaM (Option Expr)

Auxiliary method for simplifying equational theorem hypotheses.

Recall that each equation contains additional hypotheses to ensure the associated case was not taken by previous cases. We have one hypothesis for each previous case.

Equations

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