Ricardo (Feb 22 2023 at 17:33): 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.
Paolo Giarrusso (Feb 22 2023 at 17:34):You probably need erefl
Paolo Giarrusso (Feb 22 2023 at 17:34):(as a name for Logic's eq_refl)
Ricardo (Feb 22 2023 at 17:37):Paolo Giarrusso said:
You probably need erefl
Excellent. Thank you :smile:
Notification Bot (Feb 22 2023 at 17:37):Ricardo has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC