Data.DEq

A module defining the `DEq` interface

Definitions

(=?) : t -> t -> Type

Visibility: public export
Fixity Declaration: infix operator, level 1

mcong : (0 f : (a -> b)) -> x =? y -> f x =? f y

  Takes a function and an optional proof of the equality between two values
  and returns a proof of the equality between the results of that function
  applied to these values
  
  @ f   the function
  @ x y the values
  @ prf the potential proof of `x = y`

Visibility: export

mcong' : {0 f : a -> b} -> x =? y -> f x =? f y

  Like `mcong` but the function is implicit

Visibility: export

when : Bool -> a =? b -> a =? b

  When the condition holds, return the (optional) equality proof
  @ meq  the (optional) equality proof
  @ cond the condition

Visibility: export

butOnlyWhen : a =? b -> Bool -> a =? b

  Returns the (optional) equality, but only when the condition holds
  @ meq  the (optional) equality proof
  @ cond the condition

Visibility: export

and : {0 f : t -> tt -> ttt} -> a =? b -> aa =? bb -> f a aa =? f b bb

Visibility: export

interface PEq : Type -> Type

  Similar to `Eq` but the comparison operator returns a proof that the
  operands are equal (in the case where they are)
  
  The "P" in `PEq` stands for "proof"
  Note, this is not the same as `EqP` from the "some" package from Hackage

Parameters: a
Methods:

peq : (x : a) -> (y : a) -> x =? y

  Returns a proof that the operands are equal when they are,
  otherwise, returns `Nothing`

Implementations:

PEq Bool

PEq Nat

PEq Int

PEq Integer

PEq Char

PEq String

PEq a => PEq (List a)

PEq a => PEq b => PEq (a, b)

peq : PEq a => (x : a) -> (y : a) -> x =? y

  Returns a proof that the operands are equal when they are,
  otherwise, returns `Nothing`

Visibility: public export

interface DEq : (t -> Type) -> Type

  Constructors of types that allow for deciding the equality between values
  of such types, even in the case when their types are constructed from
  different parameters
  
  Modeled after the `GEq` typeclass from Haskells "some" package
  
  @ f the type constructor
  @ t the parameter type

Parameters: f
Methods:

deq : f a -> f b -> a =? b

  If the operands are equal, returns a proof, that their type parameters
  are equal

deq : DEq f => f a -> f b -> a =? b

  If the operands are equal, returns a proof, that their type parameters
  are equal

Visibility: public export

deq' : DEq f => f a -> f b -> Bool

  Compare the operands and ignore the equality proof

Visibility: export

ngeq' : DEq f => f a -> f b -> Bool

  Decide the inequality of the operands

Visibility: export