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 ...
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: Oct 13 2024 at 01:02 UTC