Default value: false
enable tactic cache debug messages (remark: they are sent to the standard error)
9.4. Options
These options affect the meaning of tactics.
option
tactic.dbg_cache
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.