How can we create an 'alias' for a tuple type in coq?
I could do
Definition alias1 := list nat.
alias1 as an alternate name for
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?
Thanks! That worked.
Ju-sh has marked this topic as resolved.
Last updated: Jan 29 2023 at 01:02 UTC