Documentation

Lean.Meta.Tactic.Constructor

source
def Lean.MVarId.constructor (mvarId : MVarId) (cfg : Meta.ApplyConfig := { }) :
MetaM (List MVarId)

When the goal mvarId type is an inductive datatype, constructor calls apply with the first matching constructor.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.MVarId.existsIntro (mvarId : MVarId) (w : Expr) :
MetaM MVarId
Equations
  • One or more equations did not get rendered due to their size.