coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] inductive definitions in Type

From: Nicolas Magaud <magaud AT unistra.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] inductive definitions in Type
Date: Mon, 15 Jan 2024 12:48:41 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=magaud AT unistra.fr; spf=Pass smtp.mailfrom=magaud AT unistra.fr; spf=None smtp.helo=postmaster AT smtpout01-ext2.partage.renater.fr
Dkim-filter: OpenDKIM Filter v2.10.3 zmtaauth03.partage.renater.fr 3B20A80196
Ironport-sdr: 65a51ba5_4VWUbq5luQNsmJDl4c9e1rPjejRuKcxOQMHnnGNlfJT+nh8 yizOKgspd6QlrAQkhhIp2bfdhVWp9Lj2KjEwUBA==

Dear Coq-club members,

In some recent experiments with Coq 8.18.0, I try and define an inductive
definition in Type. Unexpectedly, when printing the defined object, it has
type Set rather that Type.

Here are some simple examples where I would expect objects to belong to Type
(as stated in the definition) but they actually belongs to Set or Prop.

Is there any way to force them to live in Type ?

Inductive u : Type := c.
Print u.
(* Inductive u : Prop := c : u. *)

Inductive t : Type := d : nat -> t.
Print t.
(* Inductive t : Set := d : nat -> t. *)

Thanks in advance for any explanation you can provide.

Best regards,

Nicolas Magaud

[Coq-Club] inductive definitions in Type, Nicolas Magaud, 01/15/2024
- Re: [Coq-Club] inductive definitions in Type, Gaëtan Gilbert, 01/15/2024