时间戳

首页 > 解决方案 > Coq 记录类型

record - Coq 记录类型

问题描述

我是 Coq 的新手。当我尝试定义两个具有相同名称的类型字段的记录类型时，我得到一个错误。例如：

Record squag := {
    U : Type;
    op : U -> U -> U where "x * y" := (op x y);
    idempotent_op : forall x : U, (x * x) = (x);
    commutative_op : forall x y : U, (x * y) = (y * x);
    antiAbsorbent_op : forall x y: U, (x * (x * y)) = (y)
}.
Record dummy := { 
    U : Type; 
    zero : U
}.

我得到的错误是：

错误：U 已经存在。

任何帮助表示赞赏。

标签： recordcoq

解决方案

您不能在 Coq 命名空间中重复使用记录名称。但是，您可以做的是在单独的文件或模块中声明这两条记录：

Module Squag.
Record squag := {
    U : Type;
    op : U -> U -> U where "x * y" := (op x y);
    idempotent_op : forall x : U, (x * x) = (x);
    commutative_op : forall x y : U, (x * y) = (y * x);
    antiAbsorbent_op : forall x y: U, (x * (x * y)) = (y)
}.
End Squag.

Module Dummy.
Record dummy := { 
    U : Type; 
    zero : U
}.
End Dummy.

然后，您可以将这两个字段分别称为Squag.U和Dummy.U。

推荐阅读