opaque Lean.Meta.debug.terminalTacticsAsSorry : Lean.Option Bool

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

Get the user name of the given metavariable.

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

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

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

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

def Lean.Meta.mkTacticExMsg (tacticName : Name) (mvarId : MVarId) (msg : MessageData) : MessageData

Produces an error message indicating that tactic tacticName has failed with the message msg, and displays the state of mvarId below the message.

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

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

Rethrows the error as a nested error with the given tactic name prepended. If the error was tagged, prepends nested to the tag and preserves it.

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

Throw a tactic exception with given tactic name if the given metavariable is assigned.

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

Get the type the given metavariable.

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

Get the type the given metavariable after instantiating metavariables and reducing to weak head normal form.

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

Assign mvarId to sorryAx

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

Beta reduce the metavariable type head

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

Collect nondependent hypotheses that are propositions.

def Lean.Meta.saturate (mvarId : MVarId) (x : MVarId → MetaM (Option (List MVarId))) : MetaM (List MVarId)

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

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

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

Return all propositions in the local context.

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

inductive Lean.Meta.TacticResultCNM : Type

• closed : TacticResultCNM
• noChange : TacticResultCNM
• modified (mvarId : MVarId) : TacticResultCNM

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

Check if a goal is of a subsingleton type.

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