Get the user name of the given metavariable.
Equations
Instances For
Equations
Instances For
def
Lean.Meta.throwTacticEx
{α : Type}
(tacticName : Name)
(mvarId : MVarId)
(msg? : Option MessageData := none)
:
MetaM α
Equations
Instances For
Get the type the given metavariable.
Equations
Instances For
Get the type the given metavariable after instantiating metavariables and reducing to weak head normal form.
Equations
Instances For
Beta reduce the metavariable type head
Equations
Instances For
def
Lean.Meta.exactlyOne
(mvarIds : List MVarId)
(msg : MessageData := (MessageData.ofFormat ∘ format) "unexpected number of goals")
:
Equations
Instances For
def
Lean.Meta.ensureAtMostOne
(mvarIds : List MVarId)
(msg : MessageData := (MessageData.ofFormat ∘ format) "unexpected number of goals")
:
Equations
Instances For
Return all propositions in the local context.
Equations
Instances For
- closed : TacticResultCNM
- noChange : TacticResultCNM
- modified (mvarId : MVarId) : TacticResultCNM
Instances For
Check if a goal is of a subsingleton type.