Lean.Meta.Tactic.Util

source

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

Lean.MetaM Lake.Name

Get the user name of the given metavariable.

Equations

Lean.MVarId.getTag mvarId = do let __do_lift ← Lean.MVarId.getDecl mvarId pure __do_lift.userName

source

@[deprecated Lean.MVarId.getTag]

def Lean.Meta.getMVarTag (mvarId : Lean.MVarId) :

Lean.MetaM Lake.Name

Equations

Lean.Meta.getMVarTag mvarId = Lean.MVarId.getTag mvarId

source

def Lean.MVarId.setTag (mvarId : Lean.MVarId) (tag : Lake.Name) :

Lean.MetaM Unit

Equations

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

source

@[deprecated Lean.MVarId.setTag]

def Lean.Meta.setMVarTag (mvarId : Lean.MVarId) (tag : Lake.Name) :

Lean.MetaM Unit

Equations

Lean.Meta.setMVarTag mvarId tag = Lean.MVarId.setTag mvarId tag

source

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

Lake.Name

Equations

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

source

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

Lean.MetaM Unit

Equations

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

source

def Lean.Meta.mkFreshExprSyntheticOpaqueMVar (type : Lean.Expr) (tag : optParam Lake.Name Lean.Name.anonymous) :

Lean.MetaM Lean.Expr

Equations

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

source

def Lean.Meta.throwTacticEx {α : Type} (tacticName : Lake.Name) (mvarId : Lean.MVarId) (msg : Lean.MessageData) :

Lean.MetaM α

Equations

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

source

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

Lean.MetaM α

Equations

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

source

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

source

@[deprecated Lean.MVarId.checkNotAssigned]

def Lean.Meta.checkNotAssigned (mvarId : Lean.MVarId) (tacticName : Lake.Name) :

Lean.MetaM Unit

Equations

Lean.Meta.checkNotAssigned mvarId tacticName = Lean.MVarId.checkNotAssigned mvarId tacticName

source

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

Lean.MetaM Lean.Expr

Get the type the given metavariable.

Equations

Lean.MVarId.getType mvarId = do let __do_lift ← Lean.MVarId.getDecl mvarId pure __do_lift.type

source

@[deprecated Lean.MVarId.getType]

def Lean.Meta.getMVarType (mvarId : Lean.MVarId) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.getMVarType mvarId = Lean.MVarId.getType mvarId

source

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

Lean.MVarId.getType' mvarId = do let __do_lift ← Lean.MVarId.getType mvarId let __do_lift ← Lean.Meta.whnf __do_lift Lean.instantiateMVars __do_lift

source

@[deprecated Lean.MVarId.getType']

def Lean.Meta.getMVarType' (mvarId : Lean.MVarId) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.getMVarType' mvarId = Lean.MVarId.getType' mvarId

source

def Lean.MVarId.admit (mvarId : Lean.MVarId) (synthetic : optParam Bool true) :

Lean.MetaM Unit

Assign mvarId to sorryAx

Equations

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

source

@[deprecated Lean.MVarId.admit]

def Lean.Meta.admit (mvarId : Lean.MVarId) (synthetic : optParam Bool true) :

Lean.MetaM Unit

Equations

Lean.Meta.admit mvarId synthetic = Lean.MVarId.admit mvarId synthetic

source

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

Lean.MetaM Unit

Beta reduce the metavariable type head

Equations

Lean.MVarId.headBetaType mvarId = do let __do_lift ← Lean.MVarId.getType mvarId Lean.MVarId.setType mvarId (Lean.Expr.headBeta __do_lift)

source

@[deprecated Lean.MVarId.headBetaType]

def Lean.Meta.headBetaMVarType (mvarId : Lean.MVarId) :

Lean.MetaM Unit

Equations

Lean.Meta.headBetaMVarType mvarId = Lean.MVarId.headBetaType mvarId

source

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.

source

@[deprecated Lean.MVarId.getNondepPropHyps]

def Lean.Meta.getNondepPropHyps (mvarId : Lean.MVarId) :

Lean.MetaM (Array Lean.FVarId)

Equations

Lean.Meta.getNondepPropHyps mvarId = Lean.MVarId.getNondepPropHyps mvarId

source

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 ← StateRefT'.run (Lean.Meta.saturate.go x mvarId) #[] match __discr with | (fst, r) => pure (Array.toList r)

source

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

source

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

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.exactlyOne mvarIds msg = match mvarIds with | [mvarId] => pure mvarId | x => Lean.throwError msg

source

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

Lean.MetaM (Option Lean.MVarId)

Equations

Lean.Meta.ensureAtMostOne mvarIds msg = match mvarIds with | [] => pure none | [mvarId] => pure (some mvarId) | x => Lean.throwError msg

source

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.

source

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

Lean.MetaM Unit

Equations

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

source

inductive Lean.Meta.TacticResultCNM :

Type

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

source

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.

source

opaque Lean.Meta.tactic.skipAssignedInstances :

Lean.Option Bool