Ssreflect Users Discussion List

[Enrico Tassi <>]

On Thu, 2019-08-01 at 10:45 +0200, Florent Hivert wrote:
>       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 ?

Dear Florent, you are certainly right, that sentence is too ambiguous
to be useful, and you should use = in the statements of theorems like
the one above.

I've opened an issue on GH so that we don't forget clarifying what we
meant. Maybe "test" rather than "state" is more appropriate there.

Best
-- 
Enrico Tassi