我刚刚了解到'record‘关键字可以用来定义一个Prop类型,例如: Record Equivalence (A : Type) (R : relation A) : Prop := Build_Equivalence我通过Coq得到以下消息: proprecord is defined
Baa cannot be defined because it is informative and proprecord is[cannot-define-projection,records] 有人能解释一下Coq抱怨的
Coq正在使用类似于OCaml的模块系统。在OCaml中,我们可以应用像Module_A.Module_B.Func这样的函数,并使用Module_A.Module_B来查找到Func的路径。然而,我不能在Coq中做类似的事情。例如,如果我只运行Print Coq.Arith.Minus.minus_n_O.,Coq报告Coq.Arith.Minus.minus_n_O is not a defined object