如何解决我可以在coq中打印未完成证明的部分定义吗?
是否有任何命令可以打印未完成的带有元变量的证明?
例如,
Lemma a: forall P Q,(P -> Q) -> P -> Q.
intros.
apply X.
在这种证明状态下,我可以通过命令打印a := X ?
吗?
解决方法
您可以使用Show Proof
命令。在您的示例中,将显示以下内容。
(fun (P Q : Type) (X : P -> Q) (X0 : P) => X ?Goal)
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。