Get the user name of the given metavariable.
Instances For
@[deprecated Lean.MVarId.getTag]
Instances For
@[deprecated Lean.MVarId.setTag]
Instances For
Instances For
def
Lean.Meta.mkFreshExprSyntheticOpaqueMVar
(type : Lean.Expr)
(tag : optParam Lake.Name Lean.Name.anonymous)
:
Instances For
def
Lean.Meta.throwTacticEx
{α : Type}
(tacticName : Lake.Name)
(mvarId : Lean.MVarId)
(msg : Lean.MessageData)
:
Instances For
Instances For
Throw a tactic exception with given tactic name if the given metavariable is assigned.
Instances For
@[deprecated Lean.MVarId.checkNotAssigned]
Instances For
Get the type the given metavariable.
Instances For
@[deprecated Lean.MVarId.getType]
Instances For
Get the type the given metavariable after instantiating metavariables and reducing to weak head normal form.
Instances For
@[deprecated Lean.MVarId.getType']
Instances For
Assign mvarId
to sorryAx
Instances For
@[deprecated Lean.MVarId.admit]
Instances For
Beta reduce the metavariable type head
Instances For
@[deprecated Lean.MVarId.headBetaType]
Instances For
Collect nondependent hypotheses that are propositions.
Instances For
@[deprecated Lean.MVarId.getNondepPropHyps]
Instances For
def
Lean.Meta.saturate
(mvarId : Lean.MVarId)
(x : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId)))
:
Instances For
partial def
Lean.Meta.saturate.go
(x : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId)))
(mvarId : Lean.MVarId)
:
def
Lean.Meta.exactlyOne
(mvarIds : List Lean.MVarId)
(msg : optParam Lean.MessageData ((Lean.MessageData.ofFormat ∘ Std.format) "unexpected number of goals"))
:
Instances For
def
Lean.Meta.ensureAtMostOne
(mvarIds : List Lean.MVarId)
(msg : optParam Lean.MessageData ((Lean.MessageData.ofFormat ∘ Std.format) "unexpected number of goals"))
:
Instances For
Return all propositions in the local context.
Instances For
- closed: Lean.Meta.TacticResultCNM
- noChange: Lean.Meta.TacticResultCNM
- modified: Lean.MVarId → Lean.Meta.TacticResultCNM