def Lean.MVarId.constructorCore (mvarId : MVarId) (cfg : Meta.ApplyConfig := { }) (findAll : Bool := true) : MetaM (List MVarId × Array Name)

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

Along with the resulting goals, it returns the constructors that apply succeeds with, in declaration order. When findAll is false, the search stops at the first match, so at most one constructor is reported.

Equations

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

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

• mvarId.constructor cfg = do let __do_lift ← mvarId.constructorCore cfg false pure __do_lift.fst

def Lean.MVarId.existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId

Equations

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