coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Struggling wit typing

From: Helmut Brandl <helmut.brandl AT gmx.net>
To: Coq-Club <coq-club AT inria.fr>
Subject: [Coq-Club] Struggling wit typing
Date: Thu, 7 Jun 2018 21:00:12 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=helmut.brandl AT gmx.net; spf=Pass smtp.mailfrom=helmut.brandl AT gmx.net; spf=None smtp.helo=postmaster AT mout.gmx.net
Ironport-phdr: 9a23:+1Nf3BZdmXwO37SM2ao0wkz/LSx+4OfEezUN459isYplN5qZoMiybnLW6fgltlLVR4KTs6sC17KL9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa9bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjE26mHZisJ+gqFGrhy/uxNy2JTbbJ2POfdkYq/RYdEXSGxcVchRTSxBBYa8YpMNAeUfOeZYqpT9p0cTphajHwmjHuXvxSJMhnTr2qA60/ouEQXD3Aw9A9ICqm/brM/vO6cUTO+1yLLFzTrGb/JZwzv97pbHcgw4rPyKQLl+ctLRxFExGw/YkFmcs5LpMy2X2+gXrmSW7/BsWf+shmI/tQ19vjyiyt0vh4TJnI4Z107I+CZjzIooJNC1TEh2asO+HpRKrSGVLY52T9siQ252vCY6zaULuZu8fCgX1JQr3RHfa/mIcoSS5BLsSvqRLS95hHJjZr2/mw6//Va9xuHiTMW4zkhGoyhfntXRtn0BzQHf58ufRvt45Eih2DKP1w7J6uFDJEA5jarbJIAlwr41i5oTrV7PETTsmErsiq+Za0Ek9/On6+TibbTqvJmcOJFoig3mKKQhhtS/AfgkMggJR2WU5eO81KT68ULlRLVKk+Y5n7LCsJHaIMQbvrS2DxVU0oYl8Ra/Di2p3M4WnXkdfxp5f0esiJGsEFXTKrisBvCmxl+ojT1DxvbcP7SnDI+bfULOiLPwQbEo60NYzRcvi9pF7pRYDpkOJeK1XELt5/LCCRpsEwGwxvv7QP9n34USXSrbAqKdNb7O91WS7+QjJ8GDYZ9Tvjvhfat2r8XyhGM0zAdONZKi2oEaPSjhT6ZWZn6BaH+pue8vVGIDvw4wVuvv2Q+NVC4VYXuuDftlumMLTbm+BIKGfbiDxaSb1XbpEZhGIGZLFgLUSCq6R8C/Q/4JLRmqDIphnzgDDOTzTog8yVehsR+8zbd7fLLZ

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