如何解决记录为道具?
我刚刚了解到'record'关键字可用于定义Prop类型,例如:
Record Equivalence (A : Type) (R : relation A) : Prop := Build_Equivalence
{ Equivalence_Reflexive : Reflexive R;
Equivalence_Symmetric : Symmetric R;
Equivalence_Transitive : Transitive R }
但是当我尝试使用Record定义命题时,如下所示:
Record proprecord : Prop := Build_proprecord
{
Baa : nat;
Boo : Prop
}.
我收到Coq的以下消息:
proprecord is defined
Baa cannot be defined because it is informative and proprecord is not.
[cannot-define-projection,records]
Boo cannot be defined because it is informative and proprecord is not.
[cannot-define-projection,records]
任何人都可以解释Coq的抱怨-以及如何解决吗?
解决方法
对于类型为{{1}的字段,您只能获得投影函数(获取整个记录并返回单个字段的函数,例如fst
的{{1}}和snd
) },原因是您只能从prod
中提取Prop
中的内容(有一些关于singleton elimination的警告)。因此,Coq警告您不能编写函数Prop
或Prop
。
如果您希望记录的行为类似于Baa : proprecord -> nat
量词,则可以安全地忽略或消除这些警告。
您可以使用Boo proprecord -> Prop
将类型压缩为exists
,这样您就可以编写
Prop
并根据需要获取投影inhabited
和Record proprecord : Prop := Build_proprecord
{
Baa : inhabited nat;
Boo : inhabited Prop
}.
。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。