← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Relation/Unary.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/Unary.agda
25
25
 
26
26
-- I.e., they can be seen as subsets of the universe of discourse.
27
27
 
28
 
private
29
 
 module Dummy {a} {A : Set a} -- The universe of discourse.
30
 
          where
 
28
module _ {a} {A : Set a} -- The universe of discourse.
 
29
         where
31
30
 
32
31
  -- Set membership.
33
32
 
112
111
  _∩_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
113
112
  P ∩ Q = λ x → x ∈ P × x ∈ Q
114
113
 
115
 
open Dummy public
116
 
 
117
114
------------------------------------------------------------------------
118
115
-- Unary relation combinators
119
116