Get the user name of the given metavariable.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[deprecated Lean.MVarId.setTag]
Equations
- Lean.Meta.setMVarTag mvarId tag = mvarId.setTag tag
Instances For
Equations
- Lean.Meta.appendTag tag suffix = tag.modifyBase fun (x : Lake.Name) => x ++ suffix.eraseMacroScopes
Instances For
Equations
- Lean.Meta.appendTagSuffix mvarId suffix = do let tag ← mvarId.getTag mvarId.setTag (Lean.Meta.appendTag tag suffix)
Instances For
def
Lean.Meta.mkFreshExprSyntheticOpaqueMVar
(type : Lean.Expr)
(tag : optParam Lake.Name Lean.Name.anonymous)
:
Equations
Instances For
def
Lean.Meta.throwTacticEx
{α : Type}
(tacticName : Lake.Name)
(mvarId : Lean.MVarId)
(msg? : optParam (Option Lean.MessageData) none)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Throw a tactic exception with given tactic name if the given metavariable is assigned.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[deprecated Lean.MVarId.checkNotAssigned]
Equations
- Lean.Meta.checkNotAssigned mvarId tacticName = mvarId.checkNotAssigned tacticName
Instances For
Get the type the given metavariable.
Instances For
@[deprecated Lean.MVarId.getType]
Equations
- Lean.Meta.getMVarType mvarId = mvarId.getType
Instances For
Get the type the given metavariable after instantiating metavariables and reducing to weak head normal form.
Equations
- mvarId.getType' = do let __do_lift ← mvarId.getType let __do_lift ← Lean.Meta.whnf __do_lift Lean.instantiateMVars __do_lift
Instances For
@[deprecated Lean.MVarId.getType']
Equations
- Lean.Meta.getMVarType' mvarId = mvarId.getType'
Instances For
Assign mvarId
to sorryAx
Equations
- mvarId.admit synthetic = mvarId.withContext do mvarId.checkNotAssigned `admit let mvarType ← mvarId.getType let val ← Lean.Meta.mkSorry mvarType synthetic mvarId.assign val
Instances For
@[deprecated Lean.MVarId.admit]
Equations
- Lean.Meta.admit mvarId synthetic = mvarId.admit synthetic
Instances For
Beta reduce the metavariable type head
Equations
- mvarId.headBetaType = do let __do_lift ← mvarId.getType mvarId.setType __do_lift.headBeta
Instances For
@[deprecated Lean.MVarId.headBetaType]
Equations
- Lean.Meta.headBetaMVarType mvarId = mvarId.headBetaType
Instances For
Collect nondependent hypotheses that are propositions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[deprecated Lean.MVarId.getNondepPropHyps]
Equations
- Lean.Meta.getNondepPropHyps mvarId = mvarId.getNondepPropHyps
Instances For
def
Lean.Meta.saturate
(mvarId : Lean.MVarId)
(x : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId)))
:
Equations
- Lean.Meta.saturate mvarId x = do let __discr ← (Lean.Meta.saturate.go x mvarId).run #[] match __discr with | (fst, r) => pure r.toList
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"))
:
Equations
- Lean.Meta.exactlyOne mvarIds msg = match mvarIds with | [mvarId] => pure mvarId | x => Lean.throwError msg
Instances For
def
Lean.Meta.ensureAtMostOne
(mvarIds : List Lean.MVarId)
(msg : optParam Lean.MessageData ((Lean.MessageData.ofFormat ∘ Std.format) "unexpected number of goals"))
:
Equations
- Lean.Meta.ensureAtMostOne mvarIds msg = match mvarIds with | [] => pure none | [mvarId] => pure (some mvarId) | x => Lean.throwError msg
Instances For
Return all propositions in the local context.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
- closed: Lean.Meta.TacticResultCNM
- noChange: Lean.Meta.TacticResultCNM
- modified: Lean.MVarId → Lean.Meta.TacticResultCNM
Instances For
Check if a goal is of a subsingleton type.
Equations
- One or more equations did not get rendered due to their size.