0 | ||| Module with operators for the `DEq` intrerface
 1 | ||| I put them in a separate module to make it possible to avoid name
 2 | ||| ambiguities.
 3 | module Data.DEq.Operators
 4 |
 5 | import Data.DEq
 6 |
 7 | ||| Compare the operands and ignore the equality proof
 8 | ||| Alias for `deq'`
 9 | export
10 | (==) : (impl : DEq f) => f a -> f b -> Bool
11 | (==) = deq' @{impl}
12 |
13 | ||| Decide the inequality of the operands
14 | ||| Alias for `ngeq'`
15 | export
16 | (/=) : (impl : DEq f) => f a -> f b -> Bool
17 | (/=) = ngeq' @{impl}
18 |