acl2 - 在 ACL2 中禁用跳过证明警告

Question

如何在 ACL2 中禁用跳过证明警告？包括故意有很多跳过证明的书籍可能非常冗长。

Answer 1

您可以提交以下内容。

(set-inhibit-warnings "skip-proofs")

您可能希望将它放在您的 ~/acl2-customization.lisp 文件中。