Data.Comp.MultiParam.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.

Methods

pcompare :: a i -> a j -> FreshM Ordering

Instances

POrd Var

Ord a => POrd (K a)

(OrdHD f, POrd a) => POrd (Cxt h f Var a)

class EqHD f => OrdHD f where

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

Methods

compareHD :: POrd a => f Var a i -> f Var a j -> FreshM Ordering

Instances

OrdHD f => OrdHD (Cxt h f)

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

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

OrdHD is propagated through sums.