Documentation

Lean.Meta.Tactic.CasesOnStuckLHS

This module provides the casesOnStuckLHS tactic, used by

source
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
    Instances For
      source
      def Lean.Meta.casesOnStuckLHS? (mvarId : MVarId) :
      MetaM (Option (Array MVarId))
      Equations
        Instances For