Lean
维基百科,自由的 encyclopedia
Lean是一款在含归纳类型的构造演算基础上所开发的电脑证明助手(英语:Proof assistant)和函数式编程语言。[3]Lean最初由莱昂纳多·德·莫拉(英语:Leonardo de Moura)在微软研究院下研发,目前以开源合作计划的形式刊登在GitHub上。2023年成立的非盈利Lean集中研究组织(英语:Lean Focused Research Organization,缩写Lean FRO)支持Lean的持续开发。
Lean是一款在含归纳类型的构造演算基础上所开发的电脑证明助手(英语:Proof assistant)和函数式编程语言。[3]Lean最初由莱昂纳多·德·莫拉(英语:Leonardo de Moura)在微软研究院下研发,目前以开源合作计划的形式刊登在GitHub上。2023年成立的非盈利Lean集中研究组织(英语:Lean Focused Research Organization,缩写Lean FRO)支持Lean的持续开发。