Stream: Coq users

Topic: Type of constructor (in COQ reference)

Seth Chaiken (Nov 09 2023 at 17:20):

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:

Gaëtan Gilbert (Nov 09 2023 at 17:53):

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.

Seth Chaiken (Nov 09 2023 at 18:05):

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.

Paolo Giarrusso (Nov 09 2023 at 21:57):

nat->nat is indeed sugar for forall

Last updated: Oct 13 2024 at 01:02 UTC