假设我想在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))等等，但似乎没有任何效果。
您可以只写一个定义：Definition matrix := list (list nat)。该定义在大多数情况下都应该起作用（例如，您仍然可以Definition foo : matrix := [nil]使用ListNotations编写）。
如果您不想要定义（特别是因为在证明中您可能必须显式地展示一些战术的定义），则可以使用符号。正确的语法是Notation matrix := (list (list nat))。