I cannot find a standard library == function which is overloaded and returns a boolean (or a sumbool, or something I can compute with). I would like to be able to do
3==5
and
"hello" == "hello"
without having to specify the type of the arguments. I would be surprised if Coq does not have this feature for equality types; could someone tell me where to find it? I have a feeling it has something to do with ssreflect but I cannot figure it out.
Thanks.
Ssreflect has the eqType class, which has exactly what you need:
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
Check (3 == 5).
Most standard types have an equality operator defined in ssreflect. Unfortunately, strings are not one of them, though it is not to hard to roll up your own. (The Deriving library ships with an instance, but it is not marked as stable yet.)