简介
把编程和定理证明结合在一起，支持结构递归和良基递归，并为部分定义和 unsafe 定义划出明确的边界。
使用这门语言的成员
参与的讨论
partial def is the honest answer for Collatz
Lean has to know a recursive def terminates before it accepts it as a definition. Structural recursion is found automatically…
Read the axioms of a dependency's theorem before you cite it
A theorem that compiles is not yet a theorem with a proof. sorry closes any goal, and Lean accepts the file with a warning. I…