coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Struggling wit typing

From: Helmut Brandl <helmut.luis.brandl AT gmail.com>
To: Coq-Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Struggling wit typing
Date: Fri, 8 Jun 2018 10:00:55 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=helmut.luis.brandl AT gmail.com; spf=Pass smtp.mailfrom=helmut.luis.brandl AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f195.google.com
Ironport-phdr: 9a23:Elm0ah9g4JAZMv9uRHKM819IXTAuvvDOBiVQ1KB42+0cTK2v8tzYMVDF4r011RmVBdids6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+553ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRxDmiCgFNzA3/mLZhNFugq1Hux+uvQBzzpTObY2JKPZzfKXQds4aS2pbWcZRUjRMDIGiYIsLCuoBIPpYpJTgqlsUtxS+AxSjBOfywTJPhn/5w6k60+E8EQHaxgAgG88OsHXPrNnvL6gSS/q6zK/VwjXHdP5W1jL955LJchAlu/2DQbVwcc/IxEQpCgjLgFKQqYn/MDOU0OQAq2mb7+x6VeKukWErsQ9xoiKpy8wxiYfJnpoYxk7Y+Sh92oo4Jt21RFRmbdK6E5ZcrTyWOo92T84kXmpmojw1yqcctp6+ZCUKyIooxxrYa/GfdoiH+BPjVOKILTZ2nnJpZKuzhxiv/UWkyuDwTMa00FFNripKltnDqGoB2ADU6siCUvd9/0Gh1iiT1w3L9O1IPUQ5mbDYJpMh2LI8i4QfvEfZEiPrnEj7jLeadkA+9eip7+TnbK/mppiZN4JsigHxLKAumsmiAeQkKAQOW3Wb+eWn1LH55kL5Wq9Fjvsrnandq53aKsEbqbS4Aw9RyIos9xG/DzK+3NQCgXYHNE5FeA6Aj4XxJ17OJ+n4Ae6jjFSojTdk3OvLPqbhA5XINnjMiq3tfbd7605GyQo818pT55xOCuJJHPWmcUjo8ffcExVxZwez2qPsDMh3/oIYQ2OGRKGDZvD8q1iNs8IiJ+yReMc/oj/7J/xts/7jiXokhRkZYKiym5ENYXa0GtxpJkyYZTznhdJXQjRChRY3UOG/0A7KajVUfXvnB/tttAF+M5qvCML4fq7ohbWA2CmhGZgPPzJJD1mNFTHjcIDWAq5QOhLXGddol3k/bZbkU5UojEj8uwrzyr4hJe3RqHVB6MDTkeNt7uiWrikcsDx5C8PHjTOIRmBw23wSH3o4hfEi50N6zViH3O5zhPkKTdE=

Thanks for the hint.

However I cannot understand why this template polymorphism is something useful. If "sig" were defined with the type

sig: forall(A:Type) (P:A->Prop), Set

then everything would be fine.

Do I miss something?

On Fri, Jun 8, 2018, 02:58 Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

https://coq.inria.fr/distrib/current/refman/language/cic.html#template-polymorphism

Gaëtan Gilbert

On 08/06/2018 04:00, Helmut Brandl wrote:
> Hi
>
> If I type "Check sig" I get as type
>
> forall A:Type, (A->Prop) -> Type
>
> However checking the type of
>
> @sig nat (fun n => n>0).
>
> I get the type "Set". But from the type of "sig" I would expect "Type".
>
> What is wrong?
>
> Thanks
> Helmut

[Coq-Club] Struggling wit typing, Helmut Brandl, 06/08/2018
- Re: [Coq-Club] Struggling wit typing, Gaëtan Gilbert, 06/08/2018
  - Re: [Coq-Club] Struggling wit typing, Helmut Brandl, 06/08/2018
    - Re: [Coq-Club] Struggling wit typing, Gaëtan Gilbert, 06/08/2018
    - RE: [Coq-Club] Struggling wit typing, Soegtrop, Michael, 06/08/2018