Stream: Coq users

Topic: ✔ Alias for a tuple type


view this post on Zulip 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?

view this post on Zulip Pierre-Yves Strub (Nov 23 2021 at 16:03):

Try with (bool* nat)%type

view this post on Zulip Pierre-Yves Strub (Nov 23 2021 at 16:04):

https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#notation-scopes

view this post on Zulip Julin S (Nov 23 2021 at 16:04):

Thanks! That worked.

view this post on Zulip Notification Bot (Nov 23 2021 at 16:04):

Ju-sh has marked this topic as resolved.


Last updated: Jan 29 2023 at 01:02 UTC