当前位置： 首页互联网正文 本文介绍: 运行 lake build 可以构建并得到 foo 可执行文件。Lean 是一门可作为交互式定理证明工具的函数式编程语言。 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 本文来自互联网用户投稿，该文观点仅代表作者本人，不代表本站立场。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。 如若转载，请注明出处：http://www.7code.cn/show_47780.html 如若内容造成侵权/违法违规/事实不符，请联系代码007邮箱：suwngjj01@126.com进行投诉反馈，一经查实，立即删除！ 主题授权提示：请在后台主题设置-主题授权-激活主题的正版授权，授权购买：RiTheme官网显示所有内容声明：本站所有文章，如无特殊说明或标注，均为本站原创发布。任何个人或组织，在未征得本站同意时，禁止复制、盗用、采集、发布本站内容到任何网站、书籍等各类媒体平台。如若本站内容侵犯了原著者的合法权益，可联系我们进行处理。foolakelean 代码007普通 打赏 收藏 海报 链接
