受托人:[wip] LCF样式的信任内核用于经过认证的ATP和对FOLHOL的证明检查 源码

受托人 LCF样式的信任内核,用于经过认证的ATP和FOL / HOL的证明检查。 当前或正在开发的功能的简要列表: src/core/kernel.ml具有术语和定理表示的核心API。 术语将De Bruijn索引用于绑定变量,经过哈希处理,并且多态性是半显式的(即,多态常数显式应用于类型,但类型量词仍是隐式的)。 用于元语言的小型LSP服务器,位于src/lsp/ src/opentheory/一个具有解析器和基于受托者的验证者的OpenTheory库