Subject: Ssreflect Users Discussion List
List archive
- From: Florent Hivert <>
- To: "" <>
- Subject: [ssreflect] Coercion int -> rat
- Date: Thu, 14 Dec 2017 20:03:11 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=None ; spf=None
- Ironport-phdr: 9a23:Kt5NExfRYahLAhtrD7emKuDolGMj4u6mDksu8pMizoh2WeGdxcu4ZB7h7PlgxGXEQZ/co6odzbaO6ua4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahfL9+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM3/mHZhNJtgqxYrx2uuwFwzIDPbYGJKPZyYr/Rcc8ASGZfWMtaSixPApm7b4sKF+cPPeJYr47np1QQqxu+GRSnCuHuyj9WmHD2x7E62PkmHA/G2AwgGMgOv2rSrNXpLqscU+G1zLfWwjXZc/NbwjP96JLJchw7r/GMR6t9fMzMwkcsDwPIlkicpZLhMj+Py+gAsWiW4/B9We+vkWIqpAd8qSW1yMg2kInGnIcVx0jE9SpnxIY1IsW1R1B0YN64CpdQszuaN4psTsMsWWFkoCc6yrsYtp6nZCUG1YoryhrFZ/CacYWF4gjvWPuRLDtii39pYLe/iAyz8UikxO38TM600FNSoyRFltnMsWoN2ALV6sibUPdz/Eah2SiR2ADJ9uFJOkQ0lbDaK5I7zL4wjIIfsV7fES/uhEX2kKiWe10/+uiz8eTofLvmppuCOIBolgHzKb8um8y6AeQgKAcCRWmb+eKm1L3i50L1WrtKjudl2pXe5drBPt4WqKq0CBN91505rhe5FTavltUeh3gOalxfMlrTlJPzNl/KLfvkJfKkmRGtli1qzrbHOKfgC9PDNC6Qvq3meONT70lGxQwvhfBe+Z9OFvlVDvb0QEL3qJr4DwE0KRCcx/zmTttngNBNEVmTC7OUZfuB+WSD4fgidrGB
Dear all,
Is there a good reason for not having a coercion int >-> rat ?
Best,
Florent
Definition int_to_rat : int -> rat := intr.
Coercion int_to_rat : int >-> rat.
- [ssreflect] Coercion int -> rat, Florent Hivert, 12/14/2017
Archive powered by MHonArc 2.6.18.