Agda-2.6.1: A dependently typed functional programming language and proof assistant

Agda.Utils.PartialOrd

Synopsis

# Documentation

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
 Source # Instance detailsDefined in Agda.Utils.PartialOrd Methods Source # Instance detailsDefined in Agda.Utils.PartialOrd Methods Source # Instance detailsDefined in Agda.Utils.PartialOrd Methods Source # Instance detailsDefined in Agda.Utils.PartialOrd MethodsshowList :: [PartialOrdering] -> ShowS # Source # Partial ordering forms a monoid under sequencing. Instance detailsDefined in Agda.Utils.PartialOrd Methodsstimes :: Integral b => b -> PartialOrdering -> PartialOrdering # Source # Instance detailsDefined in Agda.Utils.PartialOrd Methods Source # Less is less general'' (i.e., more precise). Instance detailsDefined in Agda.Utils.PartialOrd Methods

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

Includes equality: x leqPO x == True.

Opposites.

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

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.

Chains (transitivity) x R y S z.

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

Embed Ordering.

Represent a non-empty disjunction of Orderings as PartialOrdering.

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.

Methods

Instances
 Source # Instance detailsDefined in Agda.Utils.PartialOrd Methods Source # Instance detailsDefined in Agda.Utils.PartialOrd Methods Source # Instance detailsDefined in Agda.Utils.PartialOrd Methods Source # Less is less general'' (i.e., more precise). Instance detailsDefined in Agda.Utils.PartialOrd Methods Source # Flatter is smaller. Instance detailsDefined in Agda.Syntax.Common Methods Source # More relevant is smaller. Instance detailsDefined in Agda.Syntax.Common Methods Source # Note that the order is ω ≤ 0,1, more options is smaller. Instance detailsDefined in Agda.Syntax.Common Methods Source # Dominance ordering. Instance detailsDefined in Agda.Syntax.Common Methods 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 detailsDefined in Agda.Termination.Order Methods PartialOrd a => PartialOrd (Maybe a) Source # Nothing and Just _ are unrelated.Partial ordering for Maybe a is the same as for Either () a. Instance detailsDefined in Agda.Utils.PartialOrd Methods Ord a => PartialOrd (Inclusion [a]) Source # Sublist for ordered lists. Instance detailsDefined in Agda.Utils.PartialOrd Methods Ord a => PartialOrd (Inclusion (Set a)) Source # Sets are partially ordered by inclusion. Instance detailsDefined in Agda.Utils.PartialOrd Methods 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 detailsDefined in Agda.Utils.PartialOrd Methods PartialOrd (CallMatrixAug cinfo) Source # Instance detailsDefined in Agda.Termination.CallMatrix Methods Source # Instance detailsDefined in Agda.Termination.CallMatrix Methods (PartialOrd a, PartialOrd b) => PartialOrd (Either a b) Source # Partial ordering for disjoint sums: Left _ and Right _ are unrelated. Instance detailsDefined in Agda.Utils.PartialOrd Methods (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 detailsDefined in Agda.Utils.PartialOrd Methodscomparable :: Comparable (a, b) Source # (Ord i, PartialOrd a) => PartialOrd (Matrix i a) Source # Pointwise comparison. Only matrices with the same dimension are comparable. Instance detailsDefined in Agda.Termination.SparseMatrix Methods

Any Ord is a PartialOrd.

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.

# Generic partially ordered types.

newtype Pointwise a Source #

Pointwise comparison wrapper.

Constructors

 Pointwise Fieldspointwise :: a
Instances
 Source # Instance detailsDefined in Agda.Utils.PartialOrd Methodsfmap :: (a -> b) -> Pointwise a -> Pointwise b #(<$) :: a -> Pointwise b -> Pointwise a # Eq a => Eq (Pointwise a) Source # Instance detailsDefined in Agda.Utils.PartialOrd Methods(==) :: Pointwise a -> Pointwise a -> Bool #(/=) :: Pointwise a -> Pointwise a -> Bool # Show a => Show (Pointwise a) Source # Instance detailsDefined in Agda.Utils.PartialOrd MethodsshowsPrec :: Int -> Pointwise a -> ShowS #show :: Pointwise a -> String #showList :: [Pointwise a] -> ShowS # 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 detailsDefined in Agda.Utils.PartialOrd Methods newtype Inclusion a Source # Inclusion comparison wrapper. Constructors  Inclusion Fieldsinclusion :: a Instances  Source # Instance detailsDefined in Agda.Utils.PartialOrd Methodsfmap :: (a -> b) -> Inclusion a -> Inclusion b #(<$) :: a -> Inclusion b -> Inclusion a # Eq a => Eq (Inclusion a) Source # Instance detailsDefined in Agda.Utils.PartialOrd Methods(==) :: Inclusion a -> Inclusion a -> Bool #(/=) :: Inclusion a -> Inclusion a -> Bool # Ord a => Ord (Inclusion a) Source # Instance detailsDefined in Agda.Utils.PartialOrd Methodscompare :: Inclusion a -> Inclusion a -> Ordering #(<) :: Inclusion a -> Inclusion a -> Bool #(<=) :: Inclusion a -> Inclusion a -> Bool #(>) :: Inclusion a -> Inclusion a -> Bool #(>=) :: Inclusion a -> Inclusion a -> Bool #max :: Inclusion a -> Inclusion a -> Inclusion a #min :: Inclusion a -> Inclusion a -> Inclusion a # Show a => Show (Inclusion a) Source # Instance detailsDefined in Agda.Utils.PartialOrd MethodsshowsPrec :: Int -> Inclusion a -> ShowS #show :: Inclusion a -> String #showList :: [Inclusion a] -> ShowS # Ord a => PartialOrd (Inclusion [a]) Source # Sublist for ordered lists. Instance detailsDefined in Agda.Utils.PartialOrd Methods Ord a => PartialOrd (Inclusion (Set a)) Source # Sets are partially ordered by inclusion. Instance detailsDefined in Agda.Utils.PartialOrd Methods