The manual says: https://coq.inria.fr/doc/v8.18/refman/language/core/inductive.html#type-of-constructor

"We say that is a type of constructor of I [inductive type] is one of ...

- T = (I t_1 ... t_q)
- T=forall x:U, T' where T' is also a type of constructor of I"

nat and nat->nat are given as examples for inductive type nat.

I understand how nat->nat is the type of the constructor S : nat->nat

but I don't see how nat->nat fits into one of the two cases above.

I assume nat (of O: nat) fits into the first case, nat = (nat) [with q = 0). Right?

Could someone please give an example where q>0?

Help! :smile:

for instance

```
Inductive le (n:nat) : nat -> Prop :=
| le_n : le n n
| le_S : forall m:nat, le n m -> le n S m.
```

Thanks!

I think I got the answer to my first question: U is some arity (defined a little before the quote), so nat->nat fits case 2 with nat->nat = forall x:nat, nat, and U=nat.

nat->nat is indeed sugar for forall

Last updated: Jun 13 2024 at 21:01 UTC