coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Struggling wit typing

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Struggling wit typing
Date: Fri, 8 Jun 2018 17:04:14 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay7-d.mail.gandi.net
Ironport-phdr: 9a23:jr6s/RfsRZAU4IsRPuHPv1iElGMj4u6mDksu8pMizoh2WeGdxcS7Yh7h7PlgxGXEQZ/co6odzbaO7ua4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYb5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM37X/ZisJwgqxYrhyuqRNwzIzIb4+aL/d+YqDQcMkGSWZdUMtcVSpMCZ68YYsVCOoBOP5VoYjnqFwSsRuxHw+sC/vuxD9Jgn/5xrM10/49EQrb2wEgEMgBv2rIrNrvMqceS++1zKjMzTrYcfxWwyv95ZPTchAiofCMRrFwccvUyUkqCQzFlE+cqYr7MDOJz+kAtXWQ4eRnVeKqkWEnqgdxryCuxscqkInJh5gaxkrK9SVjxos+ON62SFZjbNK6DZddtTuWOolqTs84Xm1luyg3xqcYtZKnYCQG0JUqywDFZ/Cab4SE/AjvWPueLDp7nn5pZbKyiwi0/EO90OPzTNO030xPriddktnDqHQN1xvL58idVPR9+l2u2DaN2gzK9+5IO0U0mrDaK54l2LIwmYAcsULeES/3gkn2irGZdlk89uip7eTofKnmq4eCO4NpiAzyKKYjltClDeglMQUDUXKX9fqg2LH/5UH5Ra9FjvwykqnXqpDaIsEbq7a2AwBPzIkj9wywDzG83NQXnHkHKElKdwydj4j1IFzOO/P4DPekg1SvkTdrwvXGMaP7ApnXKHjMjqvhca5n60FA0Aoz0cxf55VMB74dJ/LzQ1b9u8DcDh8kKAO52P3nCdV41oMGQ22DGK6ZMKXIsV+J/O0jOeeMZJVG8Ar6fvMi/rvliWIzsV4bZ6igm5UNO16iGfEzDEwafXPqtfgAFW0HpBZ2GOPjhUGLV3hcZnK4Urggzio4GZmlDILGS5rrhrGdinToVqZKb3xLXwjfWUzjcJ+JDq9VOXCiZ/R5mzlBboCPDooo1BWgrgj/kuQ1NenF4S4ZsJfuzp5z6vGBzEhupwwxNNyU1iS2d08xhnkBHmFkx6Nuuk98z1KOy+5+juAKTYUOtcMMaR8zMNvn98I/C932XVicLM2ETF+3HZCqRzQ4T9Z3zNYIb0c7Hdi+3EjO

Since a [sig A P] contains an A it must live at least at the level of A.
So that would be universe inconsistent.

Gaëtan Gilbert

On 08/06/2018 17:00, Helmut Brandl wrote:

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 <mailto: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