如何为 coq 中的类型指定别名

Question

假设我想在 coq 中创建一个自然数矩阵。

我有内置的 coq 列表，要创建自然数列表，我只需编写

list nat

。

为了创建一个二维列表（即矩阵），我需要编写

list (list nat)

。

我的问题是：我应该怎么做才能让 coq 完全理解

list (list nat)

这个词，就好像它是

matrix

一样？

我尝试了

---

list (list nat)

、

Notation "matrix" := list (list nat)

等，但似乎没有任何效果。

Answer 1

Notation "(matrix nat)" := (list (list nat))

。该定义应该在大多数情况下都有效（例如，您仍然可以使用 ListNotations 编写

Definition matrix := list (list nat)

）。 如果您不需要定义（特别是因为在证明中您可能必须明确展开某些策略的定义），那么您可以使用符号。正确的语法是

Definition foo : matrix := [nil]

。