Data.DOrd

A module defining the `DOrd` interface

Reexports

Definitions

data DOrdering : t -> t -> Type

  An ordering of single-parameter dependent types
  
  Modeled after the `GOrdering` type from Haskells "some" package

Totality: total
Visibility: public export
Constructors:

DLT : DOrdering a b

DEQ : DOrdering a a

DGT : DOrdering a b

ordcong' : {0 f : a -> b} -> DOrdering x y -> DOrdering (f x) (f y)

  Like `ordcong` but the function is implicit

Visibility: export

ordcong : (0 f : (a -> b)) -> DOrdering x y -> DOrdering (f x) (f y)

  Takes a function and an ordering of the two values and returns an ordering
  of the results of that function applied to these values.
  
  @ f   the function
  @ x y the values
  @ ord the ordering

Visibility: export

precedes : {0 f : t -> tt -> ttt} -> DOrdering a b -> DOrdering aa bb -> DOrdering (f a aa) (f b bb)

  ``ordL `precedes` ordR`` means that, in the resulting ordering, `ordL`
  precedes' `ordR`, that is, `ordR` is considered only if `ordL` is `DEQ`

Visibility: export

precedes' : Ordering -> DOrdering a b -> DOrdering a b

  Like `precedes`, except the preceding ordering is a regular `Ordering`

Visibility: export

interface POrd : Type -> Type

  Similar to `Ord` but the operands can be equal only when they actually are,
  that is, when the statement `p = q` is true (there is a `Refl : (p = q)`),
  where `p` and `q` are the operands
  
  The "P" in `POrd` stands for "proof"
  Note, this is not the same as `OrdP` from the "some" package from Hackage

Parameters: a
Methods:

pcompare : (x : a) -> (y : a) -> DOrdering x y

  Compare two values

Implementations:

POrd Bool

POrd Nat

POrd Int

POrd Integer

POrd Char

POrd String

POrd a => POrd (List a)

POrd a => POrd b => POrd (a, b)

pcompare : POrd a => (x : a) -> (y : a) -> DOrdering x y

  Compare two values

Visibility: public export

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

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

Parameters: f
Constraints: DEq f
Methods:

dcompare : f a -> f b -> DOrdering a b

  Compare the operands

dcompare : DOrd f => f a -> f b -> DOrdering a b

  Compare the operands

Visibility: public export

dcompare' : DOrd f => f a -> f b -> Ordering

  Compare the operands and ignore the equality proof (if the result is `DEQ`)

Visibility: export