def Lean.MVarId.getTag (mvarId : Lean.MVarId) : Lean.MetaM Lean.Name

Get the user name of the given metavariable.

Equations

• mvarId.getTag = do let __do_lift ← mvarId.getDecl pure __do_lift.userName

def Lean.MVarId.setTag (mvarId : Lean.MVarId) (tag : Lean.Name) : Lean.MetaM Unit

Equations

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

def Lean.Meta.appendTag (tag suffix : Lean.Name) : Lean.Name

Equations

• Lean.Meta.appendTag tag suffix = tag.modifyBase fun (x : Lean.Name) => x ++ suffix.eraseMacroScopes

def Lean.Meta.appendTagSuffix (mvarId : Lean.MVarId) (suffix : Lean.Name) : Lean.MetaM Unit

Equations

• Lean.Meta.appendTagSuffix mvarId suffix = do let tag ← mvarId.getTag mvarId.setTag (Lean.Meta.appendTag tag suffix)

def Lean.Meta.mkFreshExprSyntheticOpaqueMVar (type : Lean.Expr) (tag : Lean.Name := Lean.Name.anonymous) : Lean.MetaM Lean.Expr

Equations

• Lean.Meta.mkFreshExprSyntheticOpaqueMVar type tag = Lean.Meta.mkFreshExprMVar (some type) Lean.MetavarKind.syntheticOpaque tag

def Lean.Meta.throwTacticEx {α : Type} (tacticName : Lean.Name) (mvarId : Lean.MVarId) (msg? : Option Lean.MessageData := none) : Lean.MetaM α

Equations

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

def Lean.Meta.throwNestedTacticEx {α : Type} (tacticName : Lean.Name) (ex : Lean.Exception) : Lean.MetaM α

Equations

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

def Lean.MVarId.checkNotAssigned (mvarId : Lean.MVarId) (tacticName : Lean.Name) : Lean.MetaM Unit

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.

def Lean.MVarId.getType (mvarId : Lean.MVarId) : Lean.MetaM Lean.Expr

Get the type the given metavariable.

Equations

• mvarId.getType = do let __do_lift ← mvarId.getDecl pure __do_lift.type

def Lean.MVarId.getType' (mvarId : Lean.MVarId) : Lean.MetaM Lean.Expr

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

def Lean.MVarId.admit (mvarId : Lean.MVarId) (synthetic : Bool := true) : Lean.MetaM Unit

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

def Lean.MVarId.headBetaType (mvarId : Lean.MVarId) : Lean.MetaM Unit

Beta reduce the metavariable type head

Equations

• mvarId.headBetaType = do let __do_lift ← mvarId.getType mvarId.setType __do_lift.headBeta

def Lean.MVarId.getNondepPropHyps (mvarId : Lean.MVarId) : Lean.MetaM (Array Lean.FVarId)

Collect nondependent hypotheses that are propositions.

Equations

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

def Lean.Meta.saturate (mvarId : Lean.MVarId) (x : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) : Lean.MetaM (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

partial def Lean.Meta.saturate.go (x : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) (mvarId : Lean.MVarId) : StateRefT' IO.RealWorld (Array Lean.MVarId) Lean.MetaM Unit

def Lean.Meta.exactlyOne (mvarIds : List Lean.MVarId) (msg : Lean.MessageData := (Lean.MessageData.ofFormat ∘ Lean.format) "unexpected number of goals") : Lean.MetaM Lean.MVarId

Equations

• Lean.Meta.exactlyOne [mvarId] msg = pure mvarId
• Lean.Meta.exactlyOne mvarIds msg = Lean.throwError msg

def Lean.Meta.ensureAtMostOne (mvarIds : List Lean.MVarId) (msg : Lean.MessageData := (Lean.MessageData.ofFormat ∘ Lean.format) "unexpected number of goals") : Lean.MetaM (Option Lean.MVarId)

Equations

• Lean.Meta.ensureAtMostOne [] msg = pure none
• Lean.Meta.ensureAtMostOne [mvarId] msg = pure (some mvarId)
• Lean.Meta.ensureAtMostOne mvarIds msg = Lean.throwError msg

def Lean.Meta.getPropHyps : Lean.MetaM (Array Lean.FVarId)

Return all propositions in the local context.

Equations

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

def Lean.MVarId.inferInstance (mvarId : Lean.MVarId) : Lean.MetaM Unit

Equations

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

inductive Lean.Meta.TacticResultCNM : Type

• closed: Lean.Meta.TacticResultCNM
• noChange: Lean.Meta.TacticResultCNM
• modified: Lean.MVarId → Lean.Meta.TacticResultCNM

def Lean.MVarId.isSubsingleton (g : Lean.MVarId) : Lean.MetaM Bool

Check if a goal is of a subsingleton type.

Equations

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

opaque Lean.Meta.tactic.skipAssignedInstances : Lean.Option Bool