- nonDependentFirst: Lean.Meta.ApplyNewGoals
- nonDependentOnly: Lean.Meta.ApplyNewGoals
- all: Lean.Meta.ApplyNewGoals
Controls which new mvars are turned in to goals by the
nonDependentFirstmvars that don't depend on other goals appear first in the goal list.
nonDependentOnlyonly mvars that don't depend on other goals are added to goal list.
allall unassigned mvars are added to the goal list.
- newGoals : Lean.Meta.ApplyNewGoals
- synthAssignedInstances : Bool
- allowSynthFailures : Bool
- approx : Bool
approx := true, then we turn on
isDefEqapproximations. That is, we use the
Configures the behaviour of the
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.
Close the given goal using
- One or more equations did not get rendered due to their size.