Data.Comp.Ordering

This module defines ordering of signatures, which lifts to ordering of terms and contexts.

Documentation

class EqF f => OrdF f where

Signature ordering. An instance OrdF f gives rise to an instance Ord (Term f).

Methods

compareF :: Ord a => f a -> f a -> Ordering

Instances

OrdF []

OrdF Maybe

Ord a[12] => OrdF ((,) a[12])

(Ord a[12], Ord b[13]) => OrdF ((,,) a[12] b[13])

(OrdF f, OrdF g) => OrdF (:+: f g)

OrdF is propagated through sums.

OrdF f => OrdF (Cxt h f)

From an OrdF functor an Ord instance of the corresponding term type can be derived.

(Ord a[12], Ord b[13], Ord c[14]) => OrdF ((,,,) a[12] b[13] c[14])

(Ord a[12], Ord b[13], Ord c[14], Ord d[15]) => OrdF ((,,,,) a[12] b[13] c[14] d[15])

(Ord a[12], Ord b[13], Ord c[14], Ord d[15], Ord e[16]) => OrdF ((,,,,,) a[12] b[13] c[14] d[15] e[16])

(Ord a[12], Ord b[13], Ord c[14], Ord d[15], Ord e[16], Ord f[17]) => OrdF ((,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17])

(Ord a[12], Ord b[13], Ord c[14], Ord d[15], Ord e[16], Ord f[17], Ord g[18]) => OrdF ((,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18])

(Ord a[12], Ord b[13], Ord c[14], Ord d[15], Ord e[16], Ord f[17], Ord g[18], Ord h[19]) => OrdF ((,,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18] h[19])

(Ord a[12], Ord b[13], Ord c[14], Ord d[15], Ord e[16], Ord f[17], Ord g[18], Ord h[19], Ord i[1a]) => OrdF ((,,,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18] h[19] i[1a])