Agda-2.7.0: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Utils.PartialOrd

Synopsis

Documentation

data PartialOrdering Source #

The result of comparing two things (of the same type).

Constructors

POLT

Less than.

POLE

Less or equal than.

POEQ

Equal

POGE

Greater or equal.

POGT

Greater than.

POAny

No information (incomparable).

Instances

Instances details
PartialOrd PartialOrdering Source #

Less is ``less general'' (i.e., more precise).

Instance details

Defined in Agda.Utils.PartialOrd

Monoid PartialOrdering Source # 
Instance details

Defined in Agda.Utils.PartialOrd

Semigroup PartialOrdering Source #

Partial ordering forms a monoid under sequencing.

Instance details

Defined in Agda.Utils.PartialOrd

Bounded PartialOrdering Source # 
Instance details

Defined in Agda.Utils.PartialOrd

Enum PartialOrdering Source # 
Instance details

Defined in Agda.Utils.PartialOrd

Show PartialOrdering Source # 
Instance details

Defined in Agda.Utils.PartialOrd

Eq PartialOrdering Source # 
Instance details

Defined in Agda.Utils.PartialOrd

leqPO :: PartialOrdering -> PartialOrdering -> Bool Source #

Comparing the information content of two elements of PartialOrdering. More precise information is smaller.

Includes equality: x leqPO x == True.

oppPO :: PartialOrdering -> PartialOrdering Source #

Opposites.

related a po b iff related b (oppPO po) a.

orPO :: PartialOrdering -> PartialOrdering -> PartialOrdering Source #

Combining two pieces of information (picking the least information). Used for the dominance ordering on tuples.

orPO is associative, commutative, and idempotent. orPO has dominant element POAny, but no neutral element.

seqPO :: PartialOrdering -> PartialOrdering -> PartialOrdering Source #

Chains (transitivity) x R y S z.

seqPO is associative, commutative, and idempotent. seqPO has dominant element POAny and neutral element (unit) POEQ.

fromOrderings :: [Ordering] -> PartialOrdering Source #

Represent a non-empty disjunction of Orderings as PartialOrdering.

toOrderings :: PartialOrdering -> [Ordering] Source #

A PartialOrdering information is a disjunction of Ordering informations.

Comparison with partial result

type Comparable a = a -> a -> PartialOrdering Source #

class PartialOrd a where Source #

Decidable partial orderings.

Instances

Instances details
PartialOrd Cohesion Source #

Flatter is smaller.

Instance details

Defined in Agda.Syntax.Common

PartialOrd Modality Source #

Dominance ordering.

Instance details

Defined in Agda.Syntax.Common

PartialOrd Quantity Source #

Note that the order is ω ≤ 0,1, more options is smaller.

Instance details

Defined in Agda.Syntax.Common

PartialOrd Relevance Source #

More relevant is smaller.

Instance details

Defined in Agda.Syntax.Common

PartialOrd Order Source #

Information order: Unknown is least information. The more we decrease, the more information we have.

When having comparable call-matrices, we keep the lesser one. Call graph completion works toward losing the good calls, tending towards Unknown (the least information).

Instance details

Defined in Agda.Termination.Order

PartialOrd PartialOrdering Source #

Less is ``less general'' (i.e., more precise).

Instance details

Defined in Agda.Utils.PartialOrd

PartialOrd Integer Source # 
Instance details

Defined in Agda.Utils.PartialOrd

PartialOrd () Source # 
Instance details

Defined in Agda.Utils.PartialOrd

PartialOrd Int Source # 
Instance details

Defined in Agda.Utils.PartialOrd

PartialOrd t => PartialOrd (UnderAddition t) Source # 
Instance details

Defined in Agda.Syntax.Common

PartialOrd t => PartialOrd (UnderComposition t) Source # 
Instance details

Defined in Agda.Syntax.Common

PartialOrd a => PartialOrd (CallMatrix' a) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

PartialOrd (CallMatrixAug cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Ord a => PartialOrd (Inclusion (Set a)) Source #

Sets are partially ordered by inclusion.

Instance details

Defined in Agda.Utils.PartialOrd

Ord a => PartialOrd (Inclusion [a]) Source #

Sublist for ordered lists.

Instance details

Defined in Agda.Utils.PartialOrd

PartialOrd a => PartialOrd (Pointwise [a]) Source #

The pointwise ordering for lists of the same length.

There are other partial orderings for lists, e.g., prefix, sublist, subset, lexicographic, simultaneous order.

Instance details

Defined in Agda.Utils.PartialOrd

PartialOrd a => PartialOrd (Maybe a) Source #

Nothing and Just _ are unrelated.

Partial ordering for Maybe a is the same as for Either () a.

Instance details

Defined in Agda.Utils.PartialOrd

(Ord i, PartialOrd a) => PartialOrd (Matrix i a) Source #

Pointwise comparison. Only matrices with the same dimension are comparable.

Instance details

Defined in Agda.Termination.SparseMatrix

(PartialOrd a, PartialOrd b) => PartialOrd (Either a b) Source #

Partial ordering for disjoint sums: Left _ and Right _ are unrelated.

Instance details

Defined in Agda.Utils.PartialOrd

(PartialOrd a, PartialOrd b) => PartialOrd (a, b) Source #

Pointwise partial ordering for tuples.

related (x1,x2) o (y1,y2) iff related x1 o x2 and related y1 o y2.

Instance details

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable (a, b) Source #

related :: PartialOrd a => a -> PartialOrdering -> a -> Bool Source #

Are two elements related in a specific way?

related a o b holds iff comparable a b is contained in o.

Totally ordered types.

Generic partially ordered types.

newtype Pointwise a Source #

Pointwise comparison wrapper.

Constructors

Pointwise 

Fields

Instances

Instances details
Functor Pointwise Source # 
Instance details

Defined in Agda.Utils.PartialOrd

Methods

fmap :: (a -> b) -> Pointwise a -> Pointwise b #

(<$) :: a -> Pointwise b -> Pointwise a #

PartialOrd a => PartialOrd (Pointwise [a]) Source #

The pointwise ordering for lists of the same length.

There are other partial orderings for lists, e.g., prefix, sublist, subset, lexicographic, simultaneous order.

Instance details

Defined in Agda.Utils.PartialOrd

Show a => Show (Pointwise a) Source # 
Instance details

Defined in Agda.Utils.PartialOrd

Eq a => Eq (Pointwise a) Source # 
Instance details

Defined in Agda.Utils.PartialOrd

Methods

(==) :: Pointwise a -> Pointwise a -> Bool #

(/=) :: Pointwise a -> Pointwise a -> Bool #

newtype Inclusion a Source #

Inclusion comparison wrapper.

Constructors

Inclusion 

Fields

Instances

Instances details
Functor Inclusion Source # 
Instance details

Defined in Agda.Utils.PartialOrd

Methods

fmap :: (a -> b) -> Inclusion a -> Inclusion b #

(<$) :: a -> Inclusion b -> Inclusion a #

Ord a => PartialOrd (Inclusion (Set a)) Source #

Sets are partially ordered by inclusion.

Instance details

Defined in Agda.Utils.PartialOrd

Ord a => PartialOrd (Inclusion [a]) Source #

Sublist for ordered lists.

Instance details

Defined in Agda.Utils.PartialOrd

Show a => Show (Inclusion a) Source # 
Instance details

Defined in Agda.Utils.PartialOrd

Eq a => Eq (Inclusion a) Source # 
Instance details

Defined in Agda.Utils.PartialOrd

Methods

(==) :: Inclusion a -> Inclusion a -> Bool #

(/=) :: Inclusion a -> Inclusion a -> Bool #

Ord a => Ord (Inclusion a) Source # 
Instance details

Defined in Agda.Utils.PartialOrd

PartialOrdering is itself partially ordered!