def Lean.Meta.Grind.isMatchCondCandidate (e : Expr) : Bool

Returns true if e is of the form ∀ ..., _ = _ ... -> False

Equations

• Lean.Meta.Grind.isMatchCondCandidate e = Lean.Meta.Simp.isEqnThmHypothesis e

def Lean.Meta.Grind.casesMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId)

Equations

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

def Lean.Meta.Grind.casesMatch.mkMotiveAndRefls (mvarId : MVarId) (e : Expr) (app : MatcherApp) : MetaM (Expr × Array Expr)

Equations

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

def Lean.Meta.Grind.casesMatch.updateTags (mvarId : MVarId) (mvars : Array Expr) : MetaM Unit

Equations

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