← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Relation/Nullary.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-05-24 10:26:15 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110524102615-9tontf43bq9ym690
Tags: 0.5-1
http://bugs.debian.org/573807
http://bugs.debian.org/598708
* [9251e0b] Imported Upstream version 0.5
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [2c82171] Add watch file
* [0518fa6] No longer need procps | hurd BD as we no longer have the ticker
* [daf2445] Don't use upstream's make install — handled ourselves by
  dh_install
* [1b86533] Update watchfile to point at new location
* [637f47d] Remove debian/gbp.conf as we are no longer building for exp
* [cc88671] Require Agda 2.2.10
* [e99dab5] Set maximum stack size to 1G to prevent overflows in the build
* [251cd1d] Run the test suite manually
* [a7db697] Set the variable in the emacs loading script properly
* [540ca3f] Improve short description
* [6b3e794] Add dependencies on compatible versions of the Agda library
* [7127678] Standards-Version bump to 3.9.2, no changes required
* [9d0ae30] Update to use ghc instead of ghc6
* [3f6879a] Set Maintainer to my d.o email address

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Relation/Nullary.agda
2
2
-- Operations on nullary relations (like negation and decidability)
3
3
------------------------------------------------------------------------
4
4
 
5
 
{-# OPTIONS --universe-polymorphism #-}
6
 
 
7
5
-- Some operations on/properties of nullary relations, i.e. sets.
8
6
 
9
7
module Relation.Nullary where
10
8
 
11
 
open import Data.Product
12
 
open import Level
13
9
import Relation.Nullary.Core as Core
14
10
 
15
11
------------------------------------------------------------------------
18
14
open Core public using (¬_)
19
15
 
20
16
------------------------------------------------------------------------
21
 
 
22
 
infix 3 _⇔_
23
 
 
24
 
_⇔_ : ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Set ℓ₂ → Set (ℓ₁ ⊔ ℓ₂)
25
 
P ⇔ Q = (P → Q) × (Q → P)
26
 
 
27
 
------------------------------------------------------------------------
28
17
-- Decidable relations
29
18
 
30
19
open Core public using (Dec; yes; no)