11.4. Options🔗

These options affect the meaning of tactics.

option

tactic.customEliminators

Default value: true

enable using custom eliminators in the 'induction' and 'cases' tactics defined using the '@[induction_eliminator]' and '@[cases_eliminator]' attributes

option

tactic.skipAssignedInstances

Default value: true

in the rw and simp tactics, if an instance implicit argument is assigned, do not try to synthesize instance.

option

tactic.simp.trace

Default value: false

When tracing is enabled, calls to simp or dsimp will print an equivalent simp only call.