记录为道具？

问题描述

我刚刚了解到'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的抱怨-以及如何解决吗？

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）