coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gregory Malecha <gmalecha AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Canonical Structures and Coercions?
- Date: Sat, 29 Feb 2020 09:38:42 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f46.google.com
- Ironport-phdr: 9a23:me/vpBVv2eMZszVUIR5zX5NLINfV8LGtZVwlr6E/grcLSJyIuqrYbBeBt8tkgFKBZ4jH8fUM07OQ7/m8HzVYud3f4DgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+IA+5oAnMucQam5ZuJrotxhfGo3ZFePldyH91K16Ugxvz6cC88YJ5/S9Nofwh7clAUav7f6Q8U7NVCSktPn426sP2qxTNVBOD6XQAXGoYlBpIGBXF4wrhXpjtqCv6t/Fy1zecMMbrUL07QzWi76NsSB/1lCcKMiMy/W/LhsBsiq9QvQmsrAJjzYHKfI6VNeJ+fqLDctMcWWpBRdtaWyhYDo+hc4cDE+8NMOBfoIfgulsOtgO+ChewC+PzxDFIgXr20rc70+QnDArK2AMtEtYLvHnSsd77NrodUfqtwabHzTvNYfBY1yrj5ofUaR0uu+2AUKhqfMbN1UUiFQXIhUiQp4z/ODOV0/wAvWmB7+V+WuKvjHQnqgFsqTao3MgsjpfGiZ4Vyl/e6C50x4k1JdiiR05/f9GrDJtQuDuBOot5R8MtWWBouCIgxrIavp67eTEHxZI6zBDRbPyHdpKH4hPlVOuJLjd4hW5leLKihxmp60Sgy+r8W8+p21hJtipIisfAumwJ2hDJ6cWKSuFx8lm/1TqSzQze5eBJLEYpnqTBMZEh2KQ/lp8LvETDACD2nEL2gbeTdko+++io7/3rY7v8ppOBLoN0hA7zP6U0lsywBuQ4NQcOX2yF9uimyLLj+kj5TK1Ljv0wjKbZrIjXKdoHqqO9GQNY0YYu5wyhAzu4zdgUh3YKIVNddBKClYfpOlXOIP7iDfe4hlShiDhrx/XcMb3lHJrCMnjDn636cLZy7k5T0gszzdRF651IDbEBJer/WlXtu9zAEh85Lwu0zv77B9V6z4MSQH6AAquEMKzJqlKI/eIuI+yUZIAPojr9Kv4l5+TvjXAjg1Mdc7OpjtMrbyWTGe0uCEGEazK4idAYVGwOowAWTerwiVTEXyQFNFioWKdpySs2B4W8HM/mT4Sgi7yIlHO0G5RSa2tGA3iDFH7pc8OPXPJaO3HaGdNojjFRDevpcIQmzxz78VKjkus1Hq/v4iQd8Knb+p1w7uzXmws18GUtXcuY2mCJCWpzmzFRHmJk7OVEuUV4j2y7/+14jvhfT4EB4vpIVkIlL8eZwbAkTd/1XQ3Fc5GCT1P0Goz6UwF0dco4xpo1W2g4A8+r10mR0C+jArtTnLuOVsQ5
Hello --
Is there a way to get canonical structures and coercions to work together? Here's my toy example:
Structure EX : Type :=
{ t :> Type
; GET : t -> Prop }.
Definition foo {e : EX} := e.(GET).
Canonical Structure TrueEX : EX :=
{| GET := fun _ : bool => true |}.
Definition to_bool (n : nat) :=
match n with
| 0 => false
| _ => true
end.
Coercion to_bool : nat >-> bool.
Check (foo true). (* works great! *)
Check (foo 1). (* fails *)
--
{ t :> Type
; GET : t -> Prop }.
Definition foo {e : EX} := e.(GET).
Canonical Structure TrueEX : EX :=
{| GET := fun _ : bool => true |}.
Definition to_bool (n : nat) :=
match n with
| 0 => false
| _ => true
end.
Coercion to_bool : nat >-> bool.
Check (foo true). (* works great! *)
Check (foo 1). (* fails *)
Intuitively, I would expect the term [@foo boolEX (to_bool 1)] but instead I get a type error "the term 1 has type nat while it is expected to have type EX".
Is there some way to make this work without making instances for, e.g. [natEX], which is the composition of [to_bool] and [foo]?
Thanks.
gregory malecha
- [Coq-Club] Canonical Structures and Coercions?, Gregory Malecha, 02/29/2020
- Re: [Coq-Club] Canonical Structures and Coercions?, Beta Ziliani, 02/29/2020
- Re: [Coq-Club] Canonical Structures and Coercions?, Gregory Malecha, 02/29/2020
- Re: [Coq-Club] Canonical Structures and Coercions?, Bas Spitters, 02/29/2020
- Re: [Coq-Club] Canonical Structures and Coercions?, Gregory Malecha, 02/29/2020
- Re: [Coq-Club] Canonical Structures and Coercions?, Beta Ziliani, 02/29/2020
Archive powered by MHonArc 2.6.18.