Lean.Meta.Tactic.Apply

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

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 : Array Lean.Expr) (body : Lean.Expr) => pure (xs.size, body.getAppFn.isMVar))

source

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

source

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

Lean.MetaM Unit

Equations

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

source

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.

source

def Lean.Meta.postprocessAppMVars (tacticName : Lake.Name) (mvarId : Lean.MVarId) (newMVars : Array Lean.Expr) (binderInfos : Array Lean.BinderInfo) (synthAssignedInstances : optParam Bool true) (allowSynthFailures : optParam Bool false) :

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.

source

def Lean.MVarId.apply (mvarId : Lean.MVarId) (e : Lean.Expr) (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, 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.

source

@[irreducible]

def Lean.MVarId.apply.go (mvarId : Lean.MVarId) (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, 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.

source

@[deprecated Lean.MVarId.apply]

def Lean.Meta.apply (mvarId : Lean.MVarId) (e : Lean.Expr) (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true }) :

Lean.MetaM (List Lean.MVarId)

Equations

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

source

def Lean.MVarId.applyConst (mvar : Lean.MVarId) (c : Lake.Name) (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true }) :

Lean.MetaM (List Lean.MVarId)

Short-hand for applying a constant to the goal.

Equations

mvar.applyConst c cfg = do let __do_lift ← Lean.Meta.mkConstWithFreshMVarLevels c mvar.apply __do_lift cfg

source

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

Lean.MetaM (List Lean.MVarId)

Equations

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

source

partial def Lean.MVarId.splitAndCore.go (tag : Lake.Name) (type : Lean.Expr) :

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

source

@[reducible, inline]

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

Lean.MetaM (List Lean.MVarId)

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

Equations

mvarId.splitAnd = mvarId.splitAndCore

source

@[deprecated Lean.MVarId.splitAnd]

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

Lean.MetaM (List Lean.MVarId)

Equations

Lean.Meta.splitAnd mvarId = mvarId.splitAnd

source

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

Lean.MetaM Lean.MVarId

Equations

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

source

def Lean.MVarId.nthConstructor (name : Lake.Name) (idx : Nat) (expected? : optParam (Option Nat) none) (goal : Lean.MVarId) :

Lean.MetaM (List Lean.MVarId)

Apply the n-th constructor of the target type, checking that it is an inductive type, and that there are the expected number of constructors.

Equations

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

source

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

Lean.MetaM Lean.MVarId

Try to convert an Iff into an Eq by applying iff_of_eq. If successful, returns the new goal, and otherwise returns the original MVarId.

This may be regarded as being a special case of Lean.MVarId.liftReflToEq, specifically for Iff.

Equations

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

source

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

Lean.MetaM Lean.MVarId

Try to convert an Eq into an Iff by applying propext. If successful, then returns then new goal, otherwise returns the original MVarId.

Equations

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

source

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

Lean.MetaM Bool

Try to close the goal using proof_irrel_heq. Returns whether or not it succeeds.

We need to be somewhat careful not to assign metavariables while doing this, otherwise we might specialize Sort _ to Prop.

Equations

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

source

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

Lean.MetaM Bool

Try to close the goal using Subsingleton.elim. Returns whether or not it succeeds.

We are careful to apply Subsingleton.elim in a way that does not assign any metavariables. This is to prevent the Subsingleton Prop instance from being used as justification to specialize Sort _ to Prop.

Equations

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