Lean是什么？
创建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进行投诉反馈，一经查实，立即删除！
声明：本站所有文章，如无特殊说明或标注，均为本站原创发布。任何个人或组织，在未征得本站同意时，禁止复制、盗用、采集、发布本站内容到任何网站、书籍等各类媒体平台。如若本站内容侵犯了原著者的合法权益，可联系我们进行处理。
