记录是道具吗？
记录是道具吗？
提问于 2020-09-02 22:53:37
我刚刚了解到'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 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
Stack Overflow用户
回答已采纳
发布于 2020-09-03 00:46:30
对于类型为Prop的字段，您只能获得投影函数(获取全部记录并返回单个字段的函数，如prod的fst和snd )，原因是您只能从Prop中获取Prop中的内容(对所谓的singleton elimination有一些注意事项)。因此，Coq警告您它不能编写函数Baa : proprecord -> nat或Boo proprecord -> Prop。
如果您希望您的记录的行为类似于exists量词，则可以安全地忽略或静默这些警告。
您可以使用inhabited将类型压缩到Prop中，这样您就可以编写
Record proprecord : Prop := Build_proprecord
{
Baa : inhabited nat;
Boo : inhabited Prop
}.并获得预测Baa : proprecord -> inhabited nat和Boo : proprecord -> inhabited Prop，如果这是你想要的。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/63708142
复制相关文章
相似问题
腾讯云开发者
