如何在 Coq 中为类型起一个别名？

Question

假设我想在Coq中创建一个自然数矩阵。使用内置的Coq List，要创建一个自然数列表，只需要编写list nat。

为了创建一个二维列表（即矩阵），需要编写list (list nat)。

我的问题是：除了编写list (list nat)之外，我应该怎么做才能让Coq将单词matrix确切地理解为list (list nat)呢？

我尝试过Notation "matrix" := list (list nat)，Notation "(matrix nat)" := (list (list nat))等，但都没有起作用。

- Daniel

Answer 1

您可以简单地写出一个定义：定义 matrix ：= list（list nat）。该定义应该大部分情况下都有效（例如，您仍然可以使用ListNotations编写定义 foo：matrix：= [nil] ）。

如果您不想要一个定义（特别是因为在证明中，您可能需要显式展开某些策略的定义），那么您可以使用符号表示法。正确的语法是记法 matrix：=（list（list nat））。

- Tej Chajed