coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Prop / Type (again)

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Prop / Type (again)
Date: Sun, 15 Dec 2019 02:27:14 +0000
Accept-language: en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=lP4vuU7y/nJhwuC15ovenz5wr5cVFuAzXswSbldYX6c=; b=UdANmyau5ZNoOYXOYZ77Fu9OZWriut2JAawQLNaLkNvhyOKNjePIgalvaN5KK85V1yE1Tqfe+UyP1uK6r70tM3WJQarzMm85gBJR8k9uWtdzgofLhkfJ4+aI4uHdS3cpOWw5xG/5DWgS0hMr64FAoQImD6Kw8D2k78zluHvzWIav/o/CTZTYU7uCt1Nm+0FZq6H6UpKvMUg/HSic7/urHoqDpxTvQ46s/LTpX+LGFdjDyK/1jPvAKGqvj2arF5Wf/W020SthFzwQwJqjASz77v9cpixCdYB0tY6ih2NPIG7hsbESaVWuRlDlhyWD2QGZelEpCQmYQrEM028eGRcm2Q==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=N361SY4mFDQSmBGhBkc0nbKr3O8gSc3S18OsZPtNZ3pk4IxMLZdDcLmo98en16B46RD5VZ+Le4WhgMN5PEXgwlzUo8O0kM0/xDtL1xwBcCg2R2PmkgOSzD5klUrHQGyNsys6wJgAlT3LGWj8QHRNH1K4vL4b6Nwe+IKkPyPE888UCLMpjuIFOM6jLq1o0DJ/FRQlq09zYJiLhPohcbs1wDvkE+NZkhklwdxXWCPQilwazDLit5Z2szglxPaw0I4AOtgZWbo1AOYyv6O2zVfYNiqguyL9TzBIww2Hzkmd5/kXDusKRrhp4AVCW3Y0y8ZBejyv/+xfwLjWWZ8OmJbntw==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:BAvqXhM/X6CRNaAAsgQl6mtUPXoX/o7sNwtQ0KIMzox0IvT9rarrMEGX3/hxlliBBdydt6sfzbCO6eu8AiQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagb75+Ngu6oRnPusUZjoZvJLs6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gyoBKjU38nzYitZogaxbvhyvugB/zYDXboGbNvV+f7/Sc9wVSmdaQsZeTDZMDp+gY4cTDecMO/tToYnnp1sJqBuzHQ2iC/31yjBWg3/33bAx3eo7HgDIxwwgGNQOu2nTodvxKqgSS/66zKzIzDnZYf1Zwzn86JPPchAnuvyDR7RwcdfLxUYxCgzFk0+cppb4Pz6M0OkGrmuV7/J4WO+gl2IrsRx9riSty8s2l4XEiIMYxkrZ+Sh3wos5PdK1RUphbdK5FJZdtzuWO5Z2T84hWW1kpTg2x74etZ61YicHy4gryhvaZvGGcIWF4RPuWeORLDtmn31qY7eyiA2u/kWkxO3xU8e030xJoyVflNTHq2oD2AbJ6sedT/tw5keh1iiL1wDU8uxJPU47m7fHJ5I827I+kZUdvVnaEi/xg0r5krWadkI5+ui08OvnZajmppmBOINukgH+KKMumtChDuskLggOXm+b+eKm2L3k4E35XLFKjvoxkqnaqpzVOcMbpquhDw9U1IYs9Qq/Ai+p3dgEh3ULMU5JdRCdg4T0NVzDIer0AeqxjlmuiDtrwurJPrzlApXDNHjDl7LhcK555UFC0go809Vf5pJOBr8POv3yVFTxtNveDhIiKQO0xfvnBM9j2YwDRGKDGLWWML7KvV+S+u0vO/WMZJMSuDvlN/cl4OfugWYlll8ZYKmmxoAaaGu4H/RjO0WWe2DggtYHEWcQvwoxVvbmiFOYUW0bW3HnFak7/3QwDJ+sJYbFXIGkxrKblm/vFZpPI2tCF1qkEHHydozCVe1aOwyIJco0sDEeWL2wA6Moygqpskeu6bd9I+/FvAERqonk0vB84fCVmB0vszVpWZfOm1qRRn15yztbDwQ927py9BQklwWzlJNgivkdLuR9ovNEVgBmasz18tciUpXXd1uEed2EDlG7Xt+hHDc9CMorxMMDaFp8HNPkiQ3f2y2tAPkekLnZXcVloJKZ5GD4IoNG81iD0aAgi1c8Rc4Wbz+vgLM5+gTOQYfUwRzAy/SaMJ8E1SuIz1+tiHKUtRgCAgd2TOPIUW1Zb1aE9dk=

On 15/12/19 12:09 am, Gaëtan Gilbert wrote:
> When you write an inductive Coq will sometimes detect that it can be
> lowered to Prop without issue
>
> >when singleton_rel is given as
> > argument to a function which requires its argument to be (... -> ... ->
> > Type), it fails.
>
> cannot reproduce, eg
>
> Check (fun _ : (forall U V _ _ _ _, Type) => _) singleton_rel.
>
> works for me
>
> Gaëtan Gilbert
>
Hi Gaetan,

Yes, thanks, I can't reproduce the problem either, now. Obviously I
misunderstood an error message, and must have changed something which
removed it.

Thanks

Jeremy

[Coq-Club] Prop / Type (again), Jeremy Dawson, 12/14/2019
- Re: [Coq-Club] Prop / Type (again), Gaëtan Gilbert, 12/14/2019
  - Re: [Coq-Club] Prop / Type (again), Jeremy Dawson, 12/15/2019