Stream: math-comp users

Topic: ✔ eq_refl


view this post on Zulip Ricardo (Feb 22 2023 at 17:33):

There's an eq_refl in Logic and another, different eq_reflin mathcomp.ssreflect.eqtype. Why is Logic's eq_refl shadowed by mathcomp's? Is Logic's eq_refl rebound under a different name in mathcomp? As far as I understand both = and == are used in mathcomp, so it seems reasonable to have both available.

view this post on Zulip Paolo Giarrusso (Feb 22 2023 at 17:34):

You probably need erefl

view this post on Zulip Paolo Giarrusso (Feb 22 2023 at 17:34):

(as a name for Logic's eq_refl)

view this post on Zulip Ricardo (Feb 22 2023 at 17:37):

Paolo Giarrusso said:

You probably need erefl

Excellent. Thank you :smile:

view this post on Zulip Notification Bot (Feb 22 2023 at 17:37):

Ricardo has marked this topic as resolved.


Last updated: Jul 23 2024 at 19:02 UTC