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?

Try with `(bool* nat)%type`

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

Thanks! That worked.

Ju-sh has marked this topic as resolved.

Last updated: Jun 18 2024 at 20:02 UTC