How can I give an alias to a type in coq

user_5348875 0
Viewed 613

Let's say I wanna to create a matrix of natural numbers in coq.

I have the built-in coq List, and to create a list of natural numbers, I just write list nat.

In order to create a 2-dimension list (i.e. a matrix), I need to write list (list nat).

My question is: instead of writing list (list nat), what should I do for coq to understand the word matrix exactly as if it was list (list nat)?

I tried Notation "matrix" := list (list nat), Notation "(matrix nat)" := (list (list nat)), etc., but nothing seems to work.

coq alias typedef
1 Answers

You can just write a definition: Definition matrix := list (list nat). The definition should just work for the most part (eg, you can still write Definition foo : matrix := [nil], with ListNotations).

If you don't want a definition (especially because in proofs you may have to explicitly unfold the definition for some tactics), then you can use a notation. The correct syntax for that is Notation matrix := (list (list nat)).

user_40845670
Related