Как я могу дать псевдоним для типа в 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). Определение должно работать по большей части (например, вы все равно можете написать Definition foo : matrix := [nil] с ListNotations).

Если вам не нужно определение (особенно потому, что в доказательствах вам, возможно, придется явно развернуть определение для некоторых тактик), тогда вы можете использовать нотацию. Правильный синтаксис для этого Notation matrix := (list (list nat)).