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 09:57:41 +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 relay4-d.mail.gandi.net
Ironport-phdr: 9a23:0THHnxaAxBCZvdXLYkpzT77/LSx+4OfEezUN459isYplN5qZr82ybnLW6fgltlLVR4KTs6sC17KL9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa9bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjAk7m/XhMx+gqFVrh2vqBNwwZLbbo6OOfpifa7QZ88WSXZPU8tTUSFKH4Oyb5EID+oEJetWrpPyoEcSrRSkAwmjHOLhyj5MhnDtw6I6yfghGhzB0QwvBd0BrmjUo8/zNKsIXuC1za3Iwi7dYPNMxTfw85PIchMhoPGXXrJwcM/RyUwxGAPflFmQr5LqPy+M2+kLrmOV4e1gVee1hG4mrQF8ujmvxsE2ionInI0Z0F7E9T9/zY0oJtO4UFZ2bcC5HJZSrS2XNZd6Ttk/T2xrtis20KAKtJq6cSQS1Zgr2xrSZ+aZf4SU/B7vTvudLSt2iX5/Zb6yhQq+/E69wePmTMa0ykxFri9dn9nMqH8N0xvT59CdSvRj+keuwzaO2g/K5u5ZO0w0kLDUK58lwrIqmZocq0LDETL3mEnsiq+ZaFkk9vCp6+ThfLrmuoeRO5Fphgz8KKgjmNCzDf4lPgUNUWWX4/mw2bni8EHhRbVFlPw2kq3XsJDAIsQbo7a0AwBP3Yk99xawFTGm3M4XnXkGKFJKYwyIj5L1O1zVO/D4Dve+g0+vkDdqwvDGO6PuAo/XInjFjrjhYa5x61RAxwor0dBf+5VUB6kdL/L0Q0/9rcDXDhskMwOv2OvnE9V81oYGWW2VGKOZMaXSsUWJ5u01OeWMapUV637BLK0u4Oerhnskk3cce7Oo1N0ZciOWBPNjdmqQ4mblhOAuEGMAsxAiBLjlgVCeWDgVaHe2Va8m+hkgC5O9DobGQ423xrqMwHHoTdVtemlaBwXUQj/TfIKeVqJUMXPAEopaijUBEIOZZcok3BCquhX9zuM5fPHX6zYbtJfm2cIz4eDPx0hrqW5ESv+F2mTIdFla23sSTmZojrt8sFd+y1KG3LI+hfFER4QKuqF5FzwiPJuZ9NRUTtD/XgWbI4WTRVKvU4njDXc0R9M1hdAHZUp8XdOvkkKb0g==

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