Ssreflect Users Discussion List

[Florent Hivert <>]

    Hi Cyril,

On Thu, Aug 01, 2019 at 01:03:39PM +0200, Cyril wrote:
> this "always" rule is in fact always valid for "`<>` vs `!=`": we prefer to
> write `_ != _` and we never use `<>` on an `eqType`. Their are some
> exceptions where we write `(_ == _) = false` as a conclusion, to make the
> pattern more general to rewrite with...
> 
> However, for "`=` vs `==`" it is actually more subtle: generally, `==` is
> used only when necessary, e.g. in the body of a boolean predicate (e.g.
> `[pred x | f x == y]` of `[forall x, exists y, f x == y]`). Otherwise we
> prefer `=` to make the lemma ready to rewrite with.

This is more or less what I had reverse engineered from the MathComp
sources. You probably should replace the sentence by this explanation in the
book.

Thanks for the clarification,

Florent