source
opaque Lean.Meta.debug.terminalTacticsAsSorry :
Lean.Option Bool
source
def Lean.MVarId.getTag (mvarId : MVarId) :
MetaM Name

Get the user name of the given metavariable.

Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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.

Equations

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

Instances For

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

- One or more equations did not get rendered due to their size.
- Lean.Meta.throwTacticEx tacticName mvarId (some msg) = Lean.throwError (Lean.Meta.mkTacticExMsg tacticName mvarId msg)

Instances For

source
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.

Equations

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

Instances For

source
def Lean.MVarId.checkNotAssigned (mvarId : MVarId) (tacticName : Name) :
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.

Instances For

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

Get the type the given metavariable.

Equations

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

Instances For

source
def Lean.MVarId.getType' (mvarId : MVarId) :
MetaM 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

Instances For

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

Assign `mvarId` to `sorryAx`

Equations

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

Instances For

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

Beta reduce the metavariable type head

Equations

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

Instances For

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

Collect nondependent hypotheses that are propositions.

Equations

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

Instances For

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

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

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

Instances For

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

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

Instances For

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

Return all propositions in the local context.

Equations

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

Instances For

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

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

Instances For

source
inductive Lean.Meta.TacticResultCNM :
Type

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

Instances For

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

Check if a goal is of a subsingleton type.

Equations

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

Instances For

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