Data.Comp.Param.Multi.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 Name

Ord a => POrd (K a)

(OrdHD f, POrd a) => POrd (Cxt h f Name 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 Name a i -> f Name a j -> FreshM Ordering

Instances

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

OrdHD is propagated through sums.

OrdHD f => OrdHD (Cxt h f)

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