← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to src/Relation/Binary/Product/NonStrictLex.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-04-10 10:30:20 UTC
  • mfrom: (2.1.7 experimental)
  • Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
  with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Relation/Binary/Product/NonStrictLex.agda
19
19
  using (_×-Rel_)
20
20
import Relation.Binary.Product.StrictLex as Strict
21
21
 
22
 
private
23
 
 module Dummy {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where
 
22
module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where
24
23
 
25
24
  ×-Lex : (_≈₁_ _≤₁_ : Rel A₁ ℓ₁) → (_≤₂_ : Rel A₂ ℓ₂) →
26
25
          Rel (A₁ × A₂) _
150
149
    }
151
150
    where open IsDecTotalOrder
152
151
 
153
 
open Dummy public
154
 
 
155
152
-- "Packages" (e.g. posets) can also be combined.
156
153
 
157
154
_×-poset_ :