← 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/Props/TotalOrder.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/Props/TotalOrder.agda
1
1
------------------------------------------------------------------------
2
2
-- The Agda standard library
3
3
--
 
4
-- Compatibility module. Pending for removal. Use
 
5
-- Relation.Binary.Properties.TotalOrder instead.
4
6
------------------------------------------------------------------------
5
7
 
6
8
open import Relation.Binary
9
10
module Relation.Binary.Props.TotalOrder
10
11
         {t₁ t₂ t₃} (T : TotalOrder t₁ t₂ t₃) where
11
12
 
12
 
open Relation.Binary.TotalOrder T
13
 
open import Relation.Binary.Consequences
14
 
 
15
 
decTotalOrder : Decidable _≈_ → DecTotalOrder _ _ _
16
 
decTotalOrder ≟ = record
17
 
  { isDecTotalOrder = record
18
 
      { isTotalOrder = isTotalOrder
19
 
      ; _≟_          = ≟
20
 
      ; _≤?_         = total+dec⟶dec reflexive antisym total ≟
21
 
      }
22
 
  }
 
13
open import Relation.Binary.Properties.TotalOrder T public