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).
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.
You can use
Include EqbNotation A B to copy the content of the module, if A and B implement module types Typ and HasEqb A. But you can only do that once in each scope. Probably, you should instead use a library that uses canonical structures or typeclasses for this job, such as ssreflect or stdpp.
Is there an existing library that provides simple typeclasses for boolean equivalence and ordering (like Haskell Eq and Ord)? I can write my own, but hope to avoid adding yet another duplicated library to the Coq world.