Subject: Ssreflect Users Discussion List
List archive
- From: Florent Hivert <>
- To: "" <>
- Subject: [ssreflect] = vs ==
- Date: Thu, 1 Aug 2019 10:45:15 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=Pass ; spf=None
- Ironport-phdr: 9a23:qjMkzh+OyioNOf9uRHKM819IXTAuvvDOBiVQ1KB41+scTK2v8tzYMVDF4r011RmVBN+duq0P07eempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffhtEiCC5bL5wIxm6sQXcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhzodNzMh/m/ZitJ+gr9Yrh2uuxNw3oDbbZqJNPZiYq/RYc8WSHBfUstXSidPApm8b4wKD+cZPehYq479p0EQohu4GQmnGeHhyj5WhnDox606z/kqHAbG0gwkGNIOqmrbrNPpNKsIU+61zbfIwivZb/NKwjr97JLIchE7rfGCR7J9aMzcwlQsGQPdllictJLpMjeP2ugQsWWW7/BsWf+vhmI9tg19vj6izdo2hIbTnIIa0FXE+D15wIkrId24T1Z2Ydu+H5tRsyGVKYR3Qt84T2FsoiY6y6cKuZChfCQSyZQnwQDQa+CffoSV/B7uUPydLSp6iX9lYr6zmha//VK9xuHgTsW01UxFritBktnCrHAN0BnT59CHRPt5+UehwyiA1wbP6u1eI040lLTbJIA7wr4sjZcTtV7DHi7slEX4lq+abl8k9fSw6+T7frXmoYeRN5RvigHkLKsulMi/DvokPQgSRGWb4uS91Lj7/ULjWrlKj/s2krPYsJ/AP8gbqLS5UEdp1dNp8A2lAjmi3d8EtXwcNhdEfgiGhs7oPUvPKbb2F73310+3ijplw/3NIpXkGY+IL37Zkb6nfLBn6kcaxhBlnv5F4JcBJLUGOv/1RgfRtcLVFANxZyKwxPzqDsk79oIAVHiTKquDMeXcqwnbtaoUP+CQadpN637GIP8/6qu21C5rqRomZaCsmKAvRjW9F/ViLV+eZCq+hs0AV2kQ7FNnEb7azWaaWDsWXE6cGqIx4jZiVtCjBIbHS5Cxxrib3WG1BM8OPzwUOhW3CX7tMr68dbIUcivCcMt7k3oKT+r5Rg==
Dear all,
Reading the MathComp book I was surprised reading at the bottom of page 125
the following sentence:
Whenever we want to state equality between two expressions, if they live
in an eqType, always use ==.
It seems to suggest that lemmas such as
Lemma subSS n m : m.+1 - n.+1 = m - n.
should be written as
Lemma subSS n m : m.+1 - n.+1 == m - n.
which doesn't look very practical. Is it a mistake or am I missing something ?
Cheers,
Florent
- [ssreflect] = vs ==, Florent Hivert, 08/01/2019
- Re: [ssreflect] = vs ==, Enrico Tassi, 08/01/2019
- Re: [ssreflect] = vs ==, Cyril Cohen, 08/01/2019
- Re: [ssreflect] = vs ==, Florent Hivert, 08/01/2019
Archive powered by MHonArc 2.6.18.