I want to use
=? for between
bool without introducing a new notation. I saw a module type EqbNotation with such definition:
Module Type EqbNotation (T:Typ)(E:HasEqb T). Infix "=?" := E.eqb (at level 70, no associativity). End EqbNotation.
How do I use this notation to satisfy following code? or is there some notation for boolean equivalence between
bool existing elsewhere?
Definition example : bool := true =? false.