如何解决虽然预计在 Coq 中输入“forall...”
基本上,我想在这个等式上做 pose (h st)
:
h : (forall st : state,(P st -> wp st) /\ sd st) ->
forall st st' : state,extract d1 / st \\ st' -> P st -> Q st'
然而,当我运行命令时,coq 告诉我:
The term "st" has type "state" while it is expected to have type
"forall st : state,(P st -> wp st) /\ sd st".
正确的步骤是什么?
解决方法
问题在于 st
是 h
的 第二个 参数,而第一个参数预计在错误中具有那种复杂的类型。您可以改为执行 pose (fun H => h H st)
。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。