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

Question

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

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

为了创建一个二维列表(即矩阵)，我需要写 list (list nat) .

我的问题是:而不是写 list (list nat) ，我该怎么做才能让coq理解matrix这个词就好像它是 list (list nat) ?

我试过 Notation "matrix" := list (list nat) , Notation "(matrix nat)" := (list (list nat))等，但似乎没有任何效果。

Answer 1

你可以写一个定义:Definition matrix := list (list nat) .该定义应该在大部分情况下都有效(例如，您仍然可以使用 ListNotations 编写 Definition foo : matrix := [nil] )。

如果您不想要定义(特别是因为在证明中您可能必须为某些策略明确展开定义)，那么您可以使用符号。正确的语法是 Notation matrix := (list (list nat)) .