- 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.
Instances For
- newGoals : Lean.Meta.ApplyNewGoals
- synthAssignedInstances : Bool
If
synthAssignedInstances
istrue
, thenapply
will synthesize instance implicit arguments even if they have assigned byisDefEq
, and then check whether the synthesized value matches the one inferred. Thecongr
tactic sets this flag to false. - allowSynthFailures : Bool
If
allowSynthFailures
istrue
, thenapply
will return instance implicit arguments for which typeclass search failed as new goals. - approx : Bool
If
approx := true
, then we turn onisDefEq
approximations. That is, we use theapproxDefEq
combinator.
Configures the behaviour of the apply
tactic.
Instances For
Compute the number of expected arguments and whether the result type is of the form (?m ...) where ?m is an unassigned metavariable.
Instances For
Instances For
Instances For
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.
Instances For
Close the given goal using apply e
.
Instances For
Equations
- One or more equations did not get rendered due to their size.