← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Coinduction.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/Coinduction.agda
1
1
------------------------------------------------------------------------
 
2
-- Basic types related to coinduction
2
3
------------------------------------------------------------------------
3
4
 
4
5
{-# OPTIONS --universe-polymorphism #-}
5
6
 
6
 
 
7
7
module Coinduction where
8
8
 
9
 
open import Level
10
 
 
11
 
infix 10 ♯_
12
 
 
13
 
codata ∞ {a} (A : Set a) : Set a where
14
 
  ♯_ : (x : A) → ∞ A
15
 
 
16
 
♭ : ∀ {a} {A : Set a} → ∞ A → A
17
 
♭ (♯ x) = x
 
9
import Level
 
10
 
 
11
------------------------------------------------------------------------
 
12
-- A type used to make recursive arguments coinductive
 
13
 
 
14
infix 1000 ♯_
 
15
 
 
16
postulate
 
17
  ∞  : ∀ {a} (A : Set a) → Set a
 
18
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
 
19
  ♭  : ∀ {a} {A : Set a} → ∞ A → A
 
20
 
 
21
{-# BUILTIN INFINITY ∞  #-}
 
22
{-# BUILTIN SHARP    ♯_ #-}
 
23
{-# BUILTIN FLAT     ♭  #-}
 
24
 
 
25
------------------------------------------------------------------------
 
26
-- Rec, a type which is analogous to the Rec type constructor used in
 
27
-- (the current version of) ΠΣ
 
28
 
 
29
data Rec {a} (A : ∞ (Set a)) : Set a where
 
30
  fold : (x : ♭ A) → Rec A
 
31
 
 
32
unfold : ∀ {a} {A : ∞ (Set a)} → Rec A → ♭ A
 
33
unfold (fold x) = x
 
34
 
 
35
{-
 
36
 
 
37
  -- If --guardedness-preserving-type-constructors is enabled one can
 
38
  -- define types like ℕ by recursion:
 
39
 
 
40
  open import Data.Sum
 
41
  open import Data.Unit
 
42
 
 
43
  ℕ : Set
 
44
  ℕ = ⊤ ⊎ Rec (♯ ℕ)
 
45
 
 
46
  zero : ℕ
 
47
  zero = inj₁ _
 
48
 
 
49
  suc : ℕ → ℕ
 
50
  suc n = inj₂ (fold n)
 
51
 
 
52
  ℕ-rec : (P : ℕ → Set) →
 
53
          P zero →
 
54
          (∀ n → P n → P (suc n)) →
 
55
          ∀ n → P n
 
56
  ℕ-rec P z s (inj₁ _)        = z
 
57
  ℕ-rec P z s (inj₂ (fold n)) = s n (ℕ-rec P z s n)
 
58
 
 
59
  -- This feature is very experimental, though: it may lead to
 
60
  -- inconsistencies.
 
61
 
 
62
-}