coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Erkki Luuk <erkkil AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Canonical structure resolution ignores coercions
- Date: Mon, 2 Jul 2018 01:07:10 +0300
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=erkkil AT gmail.com; spf=Pass smtp.mailfrom=erkkil AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f43.google.com
- Ironport-phdr: 9a23:XX0AvB31Lo5Kp45UsmDT+DRfVm0co7zxezQtwd8ZsewQK/ad9pjvdHbS+e9qxAeQG9mDtbQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYghEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiCkJOT0k/m/JlsN9l7hUrA67qhFl34LYfIOYOfxjda3dZ9MaQm9BU95eWSxbAYO8bIoPBPcHM+ZFson9pEYFoBygCgm2B+PvyT5Ihnvt0K011uQuCwDG3Ag6E90St3TUqcz4OaEPWu621KnF1SvPY+9S1Dvn64XFcgotre+RUb9za8bcxkciGgXYhVuKs4PlJSma1uEVvmib8eVgUeWvhnYiqw5rozivwt4gio7Iho4J01zE+yp0zYgvKd23T057ZtGkEJ9OuC2AK4R2RcYiT3lpuCY81LIGpYa2cDYWxJkj3RLSaPyKf5KW7h7+V+udOzh1iXx9dLK6nRmy8EygyuPmVsmz1VZHtjRKksPPtnAO1hzT7tOKSvR4/ki72DaP0xrf5f1DIUAxjabbMYIuwqYslpoPtkTOBjP5mELvjKOPakok/vWo5P/8b7X9pp6cMpd0hRvkPqQvnMy/G+U4PRIUU2iV4+TvnIHkqEb+WfBBiuA8uqjfqpHTY8oB9YCjBAoA/5wg6Bf3Kyq705xMkGMEL1NBUB2ChontfVrJJaarXr+En12wnWIzlLj9Nbr7D8CVdymRoPLaZb94rnVk5k82xNFb6YhTD+hYcv32U0718tffC01galDm86PcENx4k7gmdyeXGKbAafHdtFaJ4qQkJOzePNZI6ga4EOAs4rvVtVF8mVIZevP0j54eaXT9GfU+ZkvFOjzjhdAOFWpMtQ07HrTn
Hi
I'm probably not the first to notice that..
(*Canonical structure resolution ignores coercions*)
Parameter T S0: Prop.
Parameter s_base: S0 -> S0 -> S0.
Structure CON := mCON {dom_con:Type; ran_con:Type; con: dom_con -> ran_con}.
Canonical Structure con_s := mCON _ _ s_base.
Definition variad := T -> S0.
Parameter variad_S0:> variad -> S0.
Parameter v: variad.
Check v: S0.
Check con _ (_:S0) (_:S0).
Check con con_s v v.
Check con _ (v:S0) v.
Fail Check con _ v v.
Does anyone know how to make canonical structure resolution work w/ coercions? I need the resolution for notation overloading (and need the coercion, too)
Best
Erkki
- [Coq-Club] Canonical structure resolution ignores coercions, Erkki Luuk, 07/02/2018
- Re: [Coq-Club] Canonical structure resolution ignores coercions, Enrico Tassi, 07/02/2018
Archive powered by MHonArc 2.6.18.