coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question about inductive definitions

From: "N. Raghavendra" <nyraghu27132 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Question about inductive definitions
Date: Fri, 16 Feb 2018 15:22:04 +0530
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=nyraghu27132 AT gmail.com; spf=Pass smtp.mailfrom=nyraghu27132 AT gmail.com; spf=None smtp.helo=postmaster AT mail-pl0-f45.google.com
Ironport-phdr: 9a23:Ny+rdh1fHInwaKbQsmDT+DRfVm0co7zxezQtwd8ZseIQK/ad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiDkJOSM3/2HNhMJ+j61Urw66qhxj34LZep2ZOOZkc6/Be94RWGpPXtxWVyxEGo6wYZMBA/AcNuhEtYb9qFsOogGgBQayAuPg1yVIiWX40aYn1OkhFwHH3BY6ENIBsHTUscv5OaUPXe270qXF1jrDb/ZM1jf87IjEaAwuofaJXb9pd8fa1EchFwTAjlqKqIzlOSuY1uQXs2ia9eZgT/ygi3U9pwFwpDij3t0shZfVhoIPzVDE6Tt2wYkpJd2jUkJ7Z8CrEIdWuiqHNIV2WtsvT390tCs+0LELup62cDIXxJkm2xLTcfOKfoiQ7h7+W+udOyp0iXxhdb6lhxu/9VKsxvDzW8Wo1ltBszBLncPWtn8X0hze8siHReV5/kemwTuP0hrc6uBAIUwtjarbL4Itzqc+lpccsUnPBCD2mELxjK+ZckUr5PKk5PjgYrXjvpOcNol0hR/iMqk2hMCzHeA1PhINUmWb4+iwybzu8VHjTLhFjvA6iqzZv4rbJcQfqK65GQhV0oM75ha5Dzamys4XnXYHLFJYZh6KjZXlNl/QLP3jAve/hk6jkDZvx/zcIrLhBZDNImDZkLj9ZbZ991JcyA0rwN9D4JJUE6gNL+73Wk/sr9PVFQQ5Mgyxw+b/EtpxzIIeWWSVAq+YKqzeq1GI5vh8a9WLMYQSoXP2L+Uvz//ol34w31EHLpOkxZ8GVHftVNIga3+QbnrlnNoHHX0D9EJqSv3wgVKCTGQMPi3od6057zA/TomhCNGQaJqqhenL+mHzJJRZZmlYB1aAC36iP9GCSu0FZyKPeJA4yWYsWr2oSotn3har4lypg4F7J/bZr3VL/ano08J4srWKxEMCsAdsBsHY6FmjCmR9n2cGXTgzhfktrkl0y1PF2q990aUBSY5joshRWwJ/DqbyivRgAomrCA3Ed9aNDl2hR4f+WGxjfpcK29YLJn1FNZCigxTEhXf4BrYUk/mTAMRx/P6BmXf2IMl5xjDN06xz11Q=

Is it possible to write the definition

Inductive total (X : Type) (P : X -> Type) : Type
:= pair : forall (x : X) , (P x -> total X P).

without using parameters, that is, in the form

Inductive total : ... := ... ?

I tried

Inductive total : forall (X : Type) , (X -> Type) -> Type
:= pair : forall (X : Type) (P : X -> Type) (x : X) , P x -> total X P.

But the latter definition gives a destructor total_rect which is
different from the destructor total_rect given by the first definition.

Thanks,
Raghu.

--
N. Raghavendra
<raghu AT hri.res.in>,
http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/

[Coq-Club] Question about inductive definitions, N. Raghavendra, 02/16/2018
- Re: [Coq-Club] Question about inductive definitions, Gaëtan Gilbert, 02/16/2018
  - Re: [Coq-Club] Question about inductive definitions, N. Raghavendra, 02/16/2018