Julin S (Nov 23 2021 at 16:02): Julin S (Nov 23 2021 at 16:02):How can we create an 'alias' for a tuple type in coq?
I could do
Definition alias1 := list nat.
to make alias1 as an alternate name for list nat.
But when I tried
Definition alias2 := (bool * nat).
I got error
The term "bool" has type "Set" while it is expected to have type "nat".
Why is this error showing up? Is my syntax wrong?
Pierre-Yves Strub (Nov 23 2021 at 16:03):Try with (bool* nat)%type
Pierre-Yves Strub (Nov 23 2021 at 16:04):https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#notation-scopes
Julin S (Nov 23 2021 at 16:04):Thanks! That worked.
Notification Bot (Nov 23 2021 at 16:04):Ju-sh has marked this topic as resolved.
Last updated: Oct 01 2023 at 18:01 UTC