Stream: Coq users

Topic: From ssreflect reflected equality to a sumbool


view this post on Zulip Valentin Robert (Feb 26 2024 at 06:01):

I'm trying to implement an OrderedType for some type that was defined in a ssreflect style.
I'm admittedly a bit rusty in Coq and very rusty in ssreflect, and was wondering whether there was a less stupid way of writing the following:

  Definition eq_dec (x y : t) : {eq x y} + {~ eq x y} :=
    match @eqP _ x y with
    | ReflectT t => left t
    | ReflectF f => right f
    end.

view this post on Zulip Enrico Tassi (Feb 26 2024 at 13:12):

I think it is fine, but that lemma exists. I think decP (@eqP _ x y) or decP (x =P y) should do it.


Last updated: Jun 22 2024 at 16:02 UTC