← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic-proposed

« back to all changes in this revision

Viewing changes to src/Relation/Binary/Properties/DecTotalOrder.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 09:46:46 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805094646-zqd0c4m8ndngqg6x
Tags: 0.8-1
* [4ca6fd0] Update debian/watch to fetch tarballs from github
* [84d4313] Imported Upstream version 0.8
* [7b08243] debian/control: Require agda 2.4.x per upstream
* [37e7e10] debian/control: Standards-Version → 3.9.5, no changes required.
* [9051b9d] Run upstream's "GenerateEverything" script

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Relation/Binary/Properties/DecTotalOrder.agda
 
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
 
4
-- Properties satisfied by decidable total orders
 
5
------------------------------------------------------------------------
 
6
 
 
7
open import Relation.Binary
 
8
 
 
9
module Relation.Binary.Properties.DecTotalOrder
 
10
         {d₁ d₂ d₃} (DT : DecTotalOrder d₁ d₂ d₃) where
 
11
 
 
12
open Relation.Binary.DecTotalOrder DT hiding (trans)
 
13
import Relation.Binary.NonStrictToStrict as Conv
 
14
open Conv _≈_ _≤_
 
15
 
 
16
strictTotalOrder : StrictTotalOrder _ _ _
 
17
strictTotalOrder = record
 
18
  { isStrictTotalOrder = record
 
19
      { isEquivalence = isEquivalence
 
20
      ; trans         = trans isPartialOrder
 
21
      ; compare       = trichotomous Eq.sym _≟_ antisym total
 
22
      ; <-resp-≈      = <-resp-≈ isEquivalence ≤-resp-≈
 
23
      }
 
24
  }
 
25
 
 
26
open StrictTotalOrder strictTotalOrder public