This module provides the casesOnStuckLHS tactic, used by

• match equation compilation
• equation compilation for recursive functions

def Lean.Meta.casesOnStuckLHS (mvarId : MVarId) : MetaM (Array MVarId)

Helper method for proveCondEqThm. Given a goal of the form C.rec ... xMajor = rhs, apply cases xMajor.

Equations

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

def Lean.Meta.casesOnStuckLHS? (mvarId : MVarId) : MetaM (Option (Array MVarId))

Equations

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