def
Lean.MVarId.constructor
(mvarId : Lean.MVarId)
(cfg : optParam Lean.Meta.ApplyConfig
{ newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false,
approx := true })
:
When the goal mvarId
type is an inductive datatype,
constructor
calls apply
with the first matching constructor.
Instances For
@[deprecated Lean.MVarId.constructor]
def
Lean.Meta.constructor
(mvarId : Lean.MVarId)
(cfg : optParam Lean.Meta.ApplyConfig
{ newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false,
approx := true })
:
Instances For
Instances For
@[deprecated Lean.MVarId.existsIntro]