~ubuntu-branches/ubuntu/lucid/agda-stdlib/lucid

« back to all changes in this revision

Viewing changes to src/Relation/Binary/Props/Poset.agda

Committer: Bazaar Package Importer
Author(s): Iain Lane
Date: 2010-01-08 23:35:09 UTC
Revision ID: james.westby@ubuntu.com-20100108233509-l6ejt9xji64xysfb

Import upstream version 0.3

files added:

.boring

AllNonAsciiChars.hs

Everything.agda

GNUmakefile

GenerateEverything.hs

Header

LICENCE

README

README.agda

README.txt

README/Nat.agda

release-notes

src/Algebra

src/Algebra.agda

src/Algebra/FunctionProperties

src/Algebra/FunctionProperties.agda

src/Algebra/FunctionProperties/Core.agda

src/Algebra/Morphism.agda

src/Algebra/Operations.agda

src/Algebra/Props

src/Algebra/Props/AbelianGroup.agda

src/Algebra/Props/BooleanAlgebra.agda

src/Algebra/Props/DistributiveLattice.agda

src/Algebra/Props/Group.agda

src/Algebra/Props/Lattice.agda

src/Algebra/Props/Ring.agda

src/Algebra/RingSolver

src/Algebra/RingSolver.agda

src/Algebra/RingSolver/AlmostCommutativeRing.agda

src/Algebra/RingSolver/Lemmas.agda

src/Algebra/RingSolver/Simple.agda

src/Algebra/Structures.agda

src/Category

src/Category/Applicative

src/Category/Applicative.agda

src/Category/Applicative/Indexed.agda

src/Category/Functor.agda

src/Category/Monad

src/Category/Monad.agda

src/Category/Monad/Continuation.agda

src/Category/Monad/Identity.agda

src/Category/Monad/Indexed.agda

src/Category/Monad/Partiality.agda

src/Category/Monad/State.agda

src/Coinduction.agda

src/Data

src/Data/AVL

src/Data/AVL.agda

src/Data/AVL/IndexedMap.agda

src/Data/AVL/Sets.agda

src/Data/Bin.agda

src/Data/Bool

src/Data/Bool.agda

src/Data/Bool/Properties.agda

src/Data/Bool/Show.agda

src/Data/BoundedVec

src/Data/BoundedVec.agda

src/Data/BoundedVec/Inefficient.agda

src/Data/Char.agda

src/Data/Cofin.agda

src/Data/Colist.agda

src/Data/Conat.agda

src/Data/Covec.agda

src/Data/DifferenceList.agda

src/Data/DifferenceNat.agda

src/Data/DifferenceVec.agda

src/Data/Digit.agda

src/Data/Empty.agda

src/Data/Fin

src/Data/Fin.agda

src/Data/Fin/Dec.agda

src/Data/Fin/Props.agda

src/Data/Fin/Subset

src/Data/Fin/Subset.agda

src/Data/Fin/Subset/Props.agda

src/Data/Fin/Substitution

src/Data/Fin/Substitution.agda

src/Data/Fin/Substitution/Example.agda

src/Data/Fin/Substitution/Lemmas.agda

src/Data/Fin/Substitution/List.agda

src/Data/Function

src/Data/Function.agda

src/Data/Function/Equality.agda

src/Data/Function/Injection.agda

src/Data/Function/LeftInverse.agda

src/Data/Graph

src/Data/Graph/Acyclic.agda

src/Data/Integer

src/Data/Integer.agda

src/Data/Integer/Divisibility.agda

src/Data/Integer/Properties.agda

src/Data/List

src/Data/List.agda

src/Data/List/All

src/Data/List/All.agda

src/Data/List/All/Properties.agda

src/Data/List/Any

src/Data/List/Any.agda

src/Data/List/Any/Properties.agda

src/Data/List/Countdown.agda

src/Data/List/NonEmpty

src/Data/List/NonEmpty.agda

src/Data/List/NonEmpty/Properties.agda

src/Data/List/Properties.agda

src/Data/List/Reverse.agda

src/Data/Map.agda

src/Data/Maybe

src/Data/Maybe.agda

src/Data/Maybe/Core.agda

src/Data/Nat

src/Data/Nat.agda

src/Data/Nat/Coprimality.agda

src/Data/Nat/DivMod.agda

src/Data/Nat/Divisibility.agda

src/Data/Nat/GCD

src/Data/Nat/GCD.agda

src/Data/Nat/GCD/Lemmas.agda

src/Data/Nat/InfinitelyOften.agda

src/Data/Nat/LCM.agda

src/Data/Nat/Properties.agda

src/Data/Nat/Show.agda

src/Data/Product

src/Data/Product.agda

src/Data/Product/Record.agda

src/Data/Rational.agda

src/Data/Sets.agda

src/Data/Sign

src/Data/Sign.agda

src/Data/Sign/Properties.agda

src/Data/Star

src/Data/Star.agda

src/Data/Star/BoundedVec.agda

src/Data/Star/Decoration.agda

src/Data/Star/Environment.agda

src/Data/Star/Fin.agda

src/Data/Star/List.agda

src/Data/Star/Nat.agda

src/Data/Star/Pointer.agda

src/Data/Star/Properties.agda

src/Data/Star/Vec.agda

src/Data/Stream.agda

src/Data/String.agda

src/Data/Sum.agda

src/Data/Unit.agda

src/Data/Vec

src/Data/Vec.agda

src/Data/Vec/Equality.agda

src/Data/Vec/N-ary.agda

src/Data/Vec/Properties.agda

src/Foreign

src/Foreign/Haskell.agda

src/IO

src/IO.agda

src/IO/Primitive.agda

src/Induction

src/Induction.agda

src/Induction/Lexicographic.agda

src/Induction/Nat.agda

src/Induction/WellFounded.agda

src/Level.agda

src/Relation

src/Relation/Binary

src/Relation/Binary.agda

src/Relation/Binary/Consequences

src/Relation/Binary/Consequences.agda

src/Relation/Binary/Consequences/Core.agda

src/Relation/Binary/Core.agda

src/Relation/Binary/EqReasoning.agda

src/Relation/Binary/Flip.agda

src/Relation/Binary/HeterogeneousEquality.agda

src/Relation/Binary/InducedPreorders.agda

src/Relation/Binary/List

src/Relation/Binary/List/NonStrictLex.agda

src/Relation/Binary/List/Pointwise.agda

src/Relation/Binary/List/StrictLex.agda

src/Relation/Binary/NonStrictToStrict.agda

src/Relation/Binary/On.agda

src/Relation/Binary/OrderMorphism.agda

src/Relation/Binary/PartialOrderReasoning.agda

src/Relation/Binary/PreorderReasoning.agda

src/Relation/Binary/Product

src/Relation/Binary/Product/NonStrictLex.agda

src/Relation/Binary/Product/Pointwise.agda

src/Relation/Binary/Product/StrictLex.agda

src/Relation/Binary/PropositionalEquality

src/Relation/Binary/PropositionalEquality.agda

src/Relation/Binary/PropositionalEquality/Core.agda

src/Relation/Binary/PropositionalEquality/TrustMe.agda

src/Relation/Binary/Props

src/Relation/Binary/Props/DecTotalOrder.agda

src/Relation/Binary/Props/Poset.agda

src/Relation/Binary/Props/Preorder.agda

src/Relation/Binary/Props/StrictPartialOrder.agda

src/Relation/Binary/Props/StrictTotalOrder.agda

src/Relation/Binary/Props/TotalOrder.agda

src/Relation/Binary/Reflection.agda

src/Relation/Binary/Simple.agda

src/Relation/Binary/StrictPartialOrderReasoning.agda

src/Relation/Binary/StrictToNonStrict.agda

src/Relation/Binary/Sum.agda

src/Relation/Nullary

src/Relation/Nullary.agda

src/Relation/Nullary/Core.agda

src/Relation/Nullary/Decidable.agda

src/Relation/Nullary/Negation.agda

src/Relation/Nullary/Product.agda

src/Relation/Nullary/Sum.agda

src/Relation/Nullary/Universe.agda

src/Relation/Unary.agda

src/Size.agda

Show diffs side-by-side

added added

removed removed

src/Relation/Binary/Props/Poset.agda

------------------------------------------------------------------------

-- Properties satisfied by posets

------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

open import Relation.Binary

module Relation.Binary.Props.Poset

{p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where

open Relation.Binary.Poset P hiding (trans)

import Relation.Binary.NonStrictToStrict as Conv

open Conv _≈_ _≤_

------------------------------------------------------------------------

-- Posets can be turned into strict partial orders

strictPartialOrder : StrictPartialOrder _ _ _

strictPartialOrder = record

{ isStrictPartialOrder = record

{ isEquivalence = isEquivalence

; irrefl = irrefl

; trans = trans isPartialOrder

; <-resp-≈ = <-resp-≈ isEquivalence ≤-resp-≈

}

open StrictPartialOrder strictPartialOrder

Older »