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

• If synthAssignedInstances is true, then apply will synthesize instance implicit arguments even if they have assigned by isDefEq, and then check whether the synthesized value matches the one inferred. The congr tactic sets this flag to false.

  synthAssignedInstances : Bool

• If approx := true, then we turn on isDefEq approximations. That is, we use the approxDefEq combinator.

  approx : Bool

Configures the behaviour of the apply tactic.

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) (synthAssignedInstances : Bool) : 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) (synthAssignedInstances : optParam Bool true) : Lean.MetaM Unit

If synthAssignedInstances is true, then apply will synthesize instance implicit arguments even if they have assigned by isDefEq, and then check whether the synthesized value matches the one inferred. The congr tactic sets this flag to false.

Equations

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

def Lean.MVarId.apply (mvarId : Lean.MVarId) (e : Lean.Expr) (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, approx := true }) : 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.MVarId.apply.go (mvarId : Lean.MVarId) (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, approx := true }) (targetType : Lean.Expr) (eType : Lean.Expr) (rangeNumArgs : Std.Range) (i : Nat) : Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo)

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, synthAssignedInstances := true, approx := true }) : 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.