`simp`与`simp!`的区别及`simp!`定义位置技术咨询

核心区别 #

• simp! 是 simp 的严格模式版本，它会禁用所有默认的 simp 引理集合，仅使用你显式指定的引理。
• 普通 simp 会自动加载核心库中标记为 @[simp] 的默认引理库，而 simp! 完全不依赖这些默认引理，只认你手动传入的引理或局部标记的 @[simp] 引理。

simp! 的定义逻辑 #

simp! 不是一个独立定义的战术，而是 Lean 语法解析器对感叹号后缀的通用支持：Lean 里不少战术都允许通过添加 ! 后缀切换到严格/精简模式，simp! 就是这种语法糖的产物。它等价于调用 simp 时自动启用 only 选项并清空默认引理集，比如 simp! 对应 simp only []，simp! [引理1, 引理2] 对应 simp only [引理1, 引理2]。

你找不到单独的 simp! 定义，是因为它的逻辑是由 Lean 前端语法处理模块实现的，最终还是映射到 simp 战术的严格模式调用。

更多信息获取方式 #

• 在 Lean 交互环境中输入 #help simp，会显示包含 simp! 在内的所有变体说明。
• 查看 Lean 官方文档中 simp 战术的章节，里面会提及感叹号后缀的语法作用。
• 查看 Lean 核心库的 Lean/Meta/Simp.lean 文件，能找到处理感叹号后缀的底层逻辑。

内容的提问来源于stack exchange，提问作者sortai