Documentation

Lean.Meta.Tactic.Apply

def Lean.Meta.getExpectedNumArgsAux (e : Lean.Expr) :

Lean.MetaM (Nat × Bool)

Equations

Lean.Meta.getExpectedNumArgsAux e = Lean.Meta.withDefault (Lean.Meta.forallTelescopeReducing e fun xs body => pure (Array.size xs, Lean.Expr.isMVar (Lean.Expr.getAppFn body)))

def Lean.Meta.getExpectedNumArgs (e : Lean.Expr) :

Equations

Lean.Meta.getExpectedNumArgs e = do let discr ← Lean.Meta.getExpectedNumArgsAux e match discr with | (numArgs, snd) => pure numArgs

def Lean.Meta.synthAppInstances (tacticName : Lean.Name) (mvarId : Lean.MVarId) (newMVars : Array Lean.Expr) (binderInfos : Array Lean.BinderInfo) :

Lean.MetaM Unit

Equations

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

def Lean.Meta.appendParentTag (mvarId : Lean.MVarId) (newMVars : Array Lean.Expr) (binderInfos : Array Lean.BinderInfo) :

Lean.MetaM Unit

Equations

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

def Lean.Meta.postprocessAppMVars (tacticName : Lean.Name) (mvarId : Lean.MVarId) (newMVars : Array Lean.Expr) (binderInfos : Array Lean.BinderInfo) :

Lean.MetaM Unit

Equations

Lean.Meta.postprocessAppMVars tacticName mvarId newMVars binderInfos = do Lean.Meta.synthAppInstances tacticName mvarId newMVars binderInfos Lean.Meta.appendParentTag mvarId newMVars binderInfos

inductive Lean.Meta.ApplyNewGoals:

Type

nonDependentFirst: Lean.Meta.ApplyNewGoals
nonDependentOnly: Lean.Meta.ApplyNewGoals
all: Lean.Meta.ApplyNewGoals

Controls which new mvars are turned in to goals by the apply tactic.

nonDependentFirst mvars that don't depend on other goals appear first in the goal list.
nonDependentOnly only mvars that don't depend on other goals are added to goal list.
all all unassigned mvars are added to the goal list.

structure Lean.Meta.ApplyConfig:

Type

newGoals : Lean.Meta.ApplyNewGoals

Configures the behaviour of the apply tactic.

def Lean.Meta.apply (mvarId : Lean.MVarId) (e : Lean.Expr) (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst }) :

Lean.MetaM (List Lean.MVarId)

Equations

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

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

Lean.MetaM (List Lean.MVarId)

Equations

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

partial def Lean.Meta.splitAnd.go (tag : Lean.Name) (type : Lean.Expr) :

StateRefT' IO.RealWorld (Array Lean.MVarId) Lean.MetaM Lean.Expr

def Lean.Meta.applyRefl (mvarId : Lean.MVarId) (msg : optParam Lean.MessageData (Function.comp Lean.MessageData.ofFormat Lean.format "refl failed")) :

Lean.MetaM Unit

Equations

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

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

Lean.MetaM Lean.MVarId

Equations

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