我有兴趣做一个依赖自动证明的项目，作为一种学习练习。到目前为止，我的在线搜索表明，理论上精益是要走的路。
然而，我读到的所有关于它的内容都是关于在 VS 代码或 Emacs 中将其用作证明助手。但这不是我需要的，我需要一个可以完全以编程方式与之通信的系统。IE 假设字符串进入 -> 指定可扣除性的字符串出现或类似的东西。
更准确地说，我需要能够在字符串上调用解析函数，这些函数完成了确定一组结果是否可以从输入假设中推导出来的繁重工作。
我找不到有关 Lean 能够做到这一点的文档。
我有兴趣做一个依赖自动证明的项目，作为一种学习练习。到目前为止，我的在线搜索表明，理论上精益是要走的路。
然而，我读到的所有关于它的内容都是关于在 VS 代码或 Emacs 中将其用作证明助手。但这不是我需要的，我需要一个可以完全以编程方式与之通信的系统。IE 假设字符串进入 -> 指定可扣除性的字符串出现或类似的东西。
更准确地说，我需要能够在字符串上调用解析函数，这些函数完成了确定一组结果是否可以从输入假设中推导出来的繁重工作。
我找不到有关 Lean 能够做到这一点的文档。