def Lean.Meta.getExpectedNumArgsAux (e : Lean.Expr) : Lean.MetaM (Nat × Bool)

Compute the number of expected arguments and whether the result type is of the form (?m ...) where ?m is an unassigned metavariable.

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) : Lean.MetaM Nat

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.MVarId.apply (mvarId : Lean.MVarId) (e : Lean.Expr) (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst }) : Lean.MetaM (List Lean.MVarId)

Close the given goal using apply e.

Equations

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

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

• Lean.Meta.apply mvarId e cfg = Lean.MVarId.apply mvarId e cfg

def Lean.Meta.splitAndCore (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.splitAndCore.go (tag : Lean.Name) (type : Lean.Expr) : StateRefT' IO.RealWorld (Array Lean.MVarId) Lean.MetaM Lean.Expr

@[inline]

abbrev Lean.MVarId.splitAnd (mvarId : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Apply And.intro as much as possible to goal mvarId.

Equations

• Lean.MVarId.splitAnd mvarId = Lean.Meta.splitAndCore mvarId

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

Equations

• Lean.Meta.splitAnd mvarId = Lean.MVarId.splitAnd mvarId

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

Equations

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