---
# System prepended metadata

title: Command line 框架研究
tags: [violet, lean]

---

# Command line 框架研究

- [ ] 研究 lake `CliM` 的使用方法
- [ ] 移植到 violet 上

## [lake](https://github.com/leanprover/lake/blob/master/Lake/CLI/Main.lean) 的方案

- [`ArgsT`](https://github.com/leanprover/lake/blob/257fc59a6464f5732a4f49e7dda0fc37475819fb/Lake/Util/Cli.lean#L20) 的實現
- lake [使用方式](https://github.com/leanprover/lake/blob/master/Lake/CLI/Main.lean)

## [lean4-cli](https://github.com/mhuisi/lean4-cli)

程式本身跟相應的 fork 都壞了或是 toolchain 版本太老我們不打算使用


###### tags: `violet` `lean`
