Data.Comp.Param.Ordering

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

Documentation

class PEq a => POrd a where

Ordering of parametric values.

Minimal complete definition

pcompare

Methods

pcompare :: a -> a -> FreshM Ordering

Instances

Ord a => POrd a

Defined in Data.Comp.Param.Ordering

Methods

pcompare :: a -> a -> FreshM Ordering

POrd a => POrd [a]

Defined in Data.Comp.Param.Ordering

Methods

pcompare :: [a] -> [a] -> FreshM Ordering

(OrdD f, POrd a) => POrd (Cxt h f Name a)

Defined in Data.Comp.Param.Ordering

Methods

pcompare :: Cxt h f Name a -> Cxt h f Name a -> FreshM Ordering

class EqD f => OrdD f where

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

Minimal complete definition

compareD

Methods

compareD :: POrd a => f Name a -> f Name a -> FreshM Ordering

Instances

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

OrdD is propagated through sums.

Defined in Data.Comp.Param.Ordering

Methods

compareD :: POrd a => (f :+: g) Name a -> (f :+: g) Name a -> FreshM Ordering

OrdD f => OrdD (Cxt h f)

From an OrdD difunctor an Ord instance of the corresponding term type can be derived.

Defined in Data.Comp.Param.Ordering

Methods

compareD :: POrd a => Cxt h f Name a -> Cxt h f Name a -> FreshM Ordering

compList :: [Ordering] -> Ordering

Orphan instances

(Difunctor f, OrdD f) => Ord (Term f)

Ordering of terms.

Methods

compare :: Term f -> Term f -> Ordering

(<) :: Term f -> Term f -> Bool

(<=) :: Term f -> Term f -> Bool

(>) :: Term f -> Term f -> Bool

(>=) :: Term f -> Term f -> Bool

max :: Term f -> Term f -> Term f

min :: Term f -> Term f -> Term f