The applyWith tactic

The applyWith tactic is like apply, but allows passing a custom configuration to the underlying apply operation.

def Mathlib.Tactic.manyConfig : Lean.ParserDescr

At least one configuration option for tactics.

If a configuration elaborator is defined as declare_config_elab elabMyConfig MyConfigStruct, a manyConfig syntax item cfg : TSyntax ``manyConfig can be passed to it using elabMyConfig (optConfigOf cfg).

optConfig allows zero or more options, manyConfig requires at least one option.

def Mathlib.Tactic.getManyConfigItems (c : Lean.Syntax) : Lean.TSyntaxArray `Lean.Parser.Tactic.configItem

Extracts the items from a tactic configuration, either a Mathlib.Tactic.manyConfig, Lean.Parser.Tactic.optConfig, Lean.Parser.Tactic.config, or these wrapped in null nodes.

def Mathlib.Tactic.optConfigOf (c : Lean.Syntax) : Lean.TSyntax `Lean.Parser.Tactic.optConfig

Convert manyConfig, optConfig or config syntax into optConfig, for use in a declare_config_elab elaborator.

def Mathlib.Tactic.elabApplyConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Meta.ApplyConfig

Elaborator for the configuration in apply (config := cfg) syntax.

def Mathlib.Tactic.applyWith : Lean.ParserDescr

apply e tries to match the current goal against the conclusion of e's type. If it succeeds, then the tactic returns as many subgoals as the number of premises that have not been fixed by type inference or type class resolution. Non-dependent premises are added before dependent ones.

The apply tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.

Extensions:

• • apply (config := cfg) e allows for additional configuration (see Lean.Meta.ApplyConfig):
    • newGoals controls which new goals are added by apply, in which order.
    • -synthAssignedInstances will not synthesize instance implicit arguments if they have been assigned by isDefEq.
    • +allowSynthFailures will create new goals when instance synthesis fails, rather than erroring.
    • +approx enables isDefEq approximations (see Lean.Meta.approxDefEq).