Safe Haskell  Safe 

Language  Haskell2010 
Synopsis
 data PartialOrdering
 leqPO :: PartialOrdering > PartialOrdering > Bool
 oppPO :: PartialOrdering > PartialOrdering
 orPO :: PartialOrdering > PartialOrdering > PartialOrdering
 seqPO :: PartialOrdering > PartialOrdering > PartialOrdering
 fromOrdering :: Ordering > PartialOrdering
 fromOrderings :: [Ordering] > PartialOrdering
 toOrderings :: PartialOrdering > [Ordering]
 type Comparable a = a > a > PartialOrdering
 class PartialOrd a where
 comparable :: Comparable a
 comparableOrd :: Ord a => Comparable a
 related :: PartialOrd a => a > PartialOrdering > a > Bool
 newtype Pointwise a = Pointwise {
 pointwise :: a
 newtype Inclusion a = Inclusion {
 inclusion :: a
Documentation
data PartialOrdering Source #
The result of comparing two things (of the same type).
POLT  Less than. 
POLE  Less or equal than. 
POEQ  Equal 
POGE  Greater or equal. 
POGT  Greater than. 
POAny  No information (incomparable). 
Instances
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
.
fromOrdering :: Ordering > PartialOrdering Source #
Embed Ordering
.
fromOrderings :: [Ordering] > PartialOrdering Source #
Represent a nonempty disjunction of Ordering
s 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.
comparable :: Comparable a Source #
Instances
PartialOrd Int Source #  
Defined in Agda.Utils.PartialOrd  
PartialOrd Integer Source #  
Defined in Agda.Utils.PartialOrd  
PartialOrd () Source #  
Defined in Agda.Utils.PartialOrd comparable :: Comparable () Source #  
PartialOrd PartialOrdering Source #  Less is ``less general'' (i.e., more precise). 
Defined in Agda.Utils.PartialOrd  
PartialOrd Relevance Source #  More relevant is smaller. 
Defined in Agda.Syntax.Common  
PartialOrd Quantity Source #  Note that the order is 
Defined in Agda.Syntax.Common  
PartialOrd Modality Source #  Dominance ordering. 
Defined in Agda.Syntax.Common  
PartialOrd Order Source #  Information order: When having comparable callmatrices, we keep the lesser one. Call graph completion works toward losing the good calls, tending towards Unknown (the least information). 
Defined in Agda.Termination.Order  
PartialOrd a => PartialOrd (Maybe a) Source # 
Partial ordering for 
Defined in Agda.Utils.PartialOrd comparable :: Comparable (Maybe a) Source #  
Ord a => PartialOrd (Inclusion [a]) Source #  Sublist for ordered lists. 
Defined in Agda.Utils.PartialOrd comparable :: Comparable (Inclusion [a]) Source #  
Ord a => PartialOrd (Inclusion (Set a)) Source #  Sets are partially ordered by inclusion. 
Defined in Agda.Utils.PartialOrd comparable :: Comparable (Inclusion (Set a)) Source #  
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. 
Defined in Agda.Utils.PartialOrd comparable :: Comparable (Pointwise [a]) Source #  
PartialOrd (CallMatrixAug cinfo) Source #  
Defined in Agda.Termination.CallMatrix comparable :: Comparable (CallMatrixAug cinfo) Source #  
PartialOrd a => PartialOrd (CallMatrix' a) Source #  
Defined in Agda.Termination.CallMatrix comparable :: Comparable (CallMatrix' a) Source #  
(PartialOrd a, PartialOrd b) => PartialOrd (Either a b) Source #  Partial ordering for disjoint sums: 
Defined in Agda.Utils.PartialOrd comparable :: Comparable (Either a b) Source #  
(PartialOrd a, PartialOrd b) => PartialOrd (a, b) Source #  Pointwise partial ordering for tuples.

Defined in Agda.Utils.PartialOrd comparable :: Comparable (a, b) Source #  
(Ord i, PartialOrd a) => PartialOrd (Matrix i a) Source #  Pointwise comparison. Only matrices with the same dimension are comparable. 
Defined in Agda.Termination.SparseMatrix comparable :: Comparable (Matrix i a) Source # 
comparableOrd :: Ord a => Comparable a Source #
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
.
Totally ordered types.
Generic partially ordered types.
Pointwise comparison wrapper.
Instances
Functor Pointwise Source #  
Eq a => Eq (Pointwise a) Source #  
Show a => Show (Pointwise a) Source #  
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. 
Defined in Agda.Utils.PartialOrd comparable :: Comparable (Pointwise [a]) Source # 
Inclusion comparison wrapper.
Instances
Functor Inclusion Source #  
Eq a => Eq (Inclusion a) Source #  
Ord a => Ord (Inclusion a) Source #  
Defined in Agda.Utils.PartialOrd  
Show a => Show (Inclusion a) Source #  
Ord a => PartialOrd (Inclusion [a]) Source #  Sublist for ordered lists. 
Defined in Agda.Utils.PartialOrd comparable :: Comparable (Inclusion [a]) Source #  
Ord a => PartialOrd (Inclusion (Set a)) Source #  Sets are partially ordered by inclusion. 
Defined in Agda.Utils.PartialOrd comparable :: Comparable (Inclusion (Set a)) Source # 