tactic.customEliminators

默认值：true

是否允许 induction 与 cases 使用由 @[induction_eliminator] 和 @[cases_eliminator] 注册的自定义消去器。默认值为 true。

tactic.skipAssignedInstances

默认值：true

在 rw 与 simp 中，实例隐式实参已有赋值时是否跳过重新合成实例。默认值为 true。

tactic.simp.trace

默认值：false

启用追踪时，让 simp 或 dsimp 打印与当前调用等价的 simp only 调用。默认值为 false。