← Back to branch summary

~ubuntu-branches/ubuntu/saucy/agda-stdlib/saucy

« back to all changes in this revision

Viewing changes to src/Data/W.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-02-25 22:28:40 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110225222840-jt16gl302kca7h0g
Tags: 0.5-1~ubuntu1
https://launchpad.net/bugs/725364
http://bugs.debian.org/573807
http://bugs.debian.org/598708

* Upload to Ubuntu from Debian's VCS due to delays in unstable caused by
  the GHC 7 transition (LP: #725364)
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [0fb0600] Standards-Version → 3.9.1, no changes required
* [d3f13b8] Update required Agda version to 2.2.8
* [cc1f5c8] Imported Upstream version 0.4
* [2c82171] Add watch file
* [9251e0b] Imported Upstream version 0.5
* [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

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/W.agda
 
1
------------------------------------------------------------------------
 
2
-- W-types
 
3
------------------------------------------------------------------------
 
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
 
7
module Data.W where
 
8
 
 
9
open import Level
 
10
open import Relation.Nullary
 
11
 
 
12
-- The family of W-types.
 
13
 
 
14
data W {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
 
15
  sup : (x : A) (f : B x → W A B) → W A B
 
16
 
 
17
-- Projections.
 
18
 
 
19
head : ∀ {a b} {A : Set a} {B : A → Set b} →
 
20
       W A B → A
 
21
head (sup x f) = x
 
22
 
 
23
tail : ∀ {a b} {A : Set a} {B : A → Set b} →
 
24
       (x : W A B) → B (head x) → W A B
 
25
tail (sup x f) = f
 
26
 
 
27
-- If B is always inhabited, then W A B is empty.
 
28
 
 
29
inhabited⇒empty : ∀ {a b} {A : Set a} {B : A → Set b} →
 
30
                  (∀ x → B x) → ¬ W A B
 
31
inhabited⇒empty b (sup x f) = inhabited⇒empty b (f (b x))