HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

ModuleAgda-2.7.0.1Haskell2010

Agda.Utils.PartialOrd

  • 4 types
  • 1 class
  • 9 values
  • PackageAgda-2.7.0.1
  • Exports14
  • LanguageHaskell2010
  • LicenceMIT
  • SourcePartialOrd.hs
datadata PartialOrdering
#

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

Constructors

Instances7Bounded, Enum, Eq, Show, Semigroup, Monoid, …
valueorPO :: PartialOrdering -> PartialOrdering -> PartialOrdering
#

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.

Comparison with partial result

4 declarations
classclass PartialOrd a where
#

Decidable partial orderings.

Methods

Instances20PartialOrd, …
  • PartialOrd CohesionDefined in Agda-2.7.0.1 · Agda.Syntax.Common

    Flatter is smaller.

  • PartialOrd ModalityDefined in Agda-2.7.0.1 · Agda.Syntax.Common

    Dominance ordering.

  • PartialOrd QuantityDefined in Agda-2.7.0.1 · Agda.Syntax.Common

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

  • PartialOrd RelevanceDefined in Agda-2.7.0.1 · Agda.Syntax.Common

    More relevant is smaller.

  • PartialOrd OrderDefined in Agda-2.7.0.1 · Agda.Termination.Order

    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).

  • PartialOrd PartialOrderingDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd

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

  • PartialOrd IntegerDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
  • PartialOrd IntDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
  • PartialOrd ()Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
  • PartialOrd (CallMatrixAug cinfo)Defined in Agda-2.7.0.1 · Agda.Termination.CallMatrix
  • PartialOrd a => PartialOrd (CallMatrix' a)Defined in Agda-2.7.0.1 · Agda.Termination.CallMatrix
  • PartialOrd a => PartialOrd (Pointwise [a])Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd

    The pointwise ordering for lists of the same length.

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

  • PartialOrd a => PartialOrd (Maybe a)Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd

    Nothing and Just _ are unrelated.

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

  • PartialOrd t => PartialOrd (UnderAddition t)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
  • PartialOrd t => PartialOrd (UnderComposition t)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Ord a => PartialOrd (Inclusion (Set a))Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd

    Sets are partially ordered by inclusion.

  • Ord a => PartialOrd (Inclusion [a])Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd

    Sublist for ordered lists.

  • (PartialOrd a, PartialOrd b) => PartialOrd (Either a b)Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd

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

  • (PartialOrd a, PartialOrd b) => PartialOrd (a, b)Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd

    Pointwise partial ordering for tuples.

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

  • (Ord i, PartialOrd a) => PartialOrd (Matrix i a)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix

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

Totally ordered types.

0 declarations

Generic partially ordered types.

2 declarations
newtypenewtype Pointwise a
#

Pointwise comparison wrapper.

Constructors

Instances4Functor, Eq, Show, PartialOrd
  • Functor PointwiseDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
  • Eq a => Eq (Pointwise a)Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
  • Show a => Show (Pointwise a)Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
  • PartialOrd a => PartialOrd (Pointwise [a])Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd

    The pointwise ordering for lists of the same length.

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

newtypenewtype Inclusion a
#

Inclusion comparison wrapper.

Constructors

Instances6Functor, Eq, Ord, Show, PartialOrd

PartialOrdering is itself partially ordered!

0 declarations