Skip to Content.
Sympa Menu

ssreflect - [ssreflect] = vs ==

Subject: Ssreflect Users Discussion List

List archive

[ssreflect] = vs ==


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page