为何新一代依赖类型语言未采用SSReflect的设计思路？

太赞同你这个发现了！我也注意到Coq的SSReflect扩展里有两项特别实用的约定，但在Lean、Agda、Idris这类新一代依赖类型语言里并没有被广泛采用。其中第一个就非常值得说道：

1. 尽可能将谓词表示为返回布尔值的函数，而非归纳定义的数据类型 #

和大多数依赖类型语言里常用的「把谓词定义为归纳命题」的方式不同，SSReflect更倾向于用返回bool类型的函数来实现谓词。这个设计带来了不少实打实的好处：

• 自带可判定性：布尔函数本身就是可判定的，你不需要额外证明某个谓词能被计算性检查——这一点是默认就有的。
• 拓展计算式证明的场景：你可以直接在证明里利用这些布尔函数的计算行为，让「计算式推理」更流畅，感觉更贴近实际代码的逻辑。
• 提升证明检查性能：避免了让证明引擎跟踪和验证归纳证明项的额外开销，布尔值谓词能让证明检查更快，生成的证明对象也更精简。

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