def Lean.MVarId.constructor (mvarId : Lean.MVarId) (cfg : Lean.Meta.ApplyConfig := { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true }) : Lean.MetaM (List Lean.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.

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

Equations

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