Lean语言学习笔记

2023-12-13 05:34:29

Lean是什么？

Lean 是一门可作为交互式定理证明工具的函数式编程语言。

创建Lean项目

可以使用 lake 来创建一个新的 Lean 项目：

mkdir lean-playground && cd lean-playground
lake init foo

之后会得到下面的目录结构：

├── Foo
├── Foo.lean
├── lakefile.lean
├── lake-manifest.json
├── lean-toolchain
└── Main.lean

运行 lake build 可以构建并得到 foo 可执行文件。运行 ./build/bin/foo 会输出：

Hello, world!

文章来源:https://blog.csdn.net/bupt073114/article/details/134804376
本文来自互联网用户投稿，该文观点仅代表作者本人，不代表本站立场。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。