← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to test/fail/TypeConstructorsWhichPreserveGuardedness1.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
test/fail/TypeConstructorsWhichPreserveGuardedness1.agda
1
 
 
2
 
module TypeConstructorsWhichPreserveGuardedness1 where
3
 
 
4
 
open import Imports.Coinduction
5
 
 
6
 
record ⊤ : Set where
7
 
 
8
 
data _⊎_ (A B : Set) : Set where
9
 
  inj₁ : A → A ⊎ B
10
 
  inj₂ : B → A ⊎ B
11
 
 
12
 
record ∃ {A : Set} (B : A → Set) : Set where
13
 
  constructor _,_
14
 
  field
15
 
    proj₁ : A
16
 
    proj₂ : B proj₁
17
 
 
18
 
data Rec (A : ∞ Set) : Set where
19
 
  fold : ♭ A → Rec A
20
 
 
21
 
module ℕ₁ where
22
 
 
23
 
  ℕ : Set
24
 
  ℕ = ⊤ ⊎ Rec (♯ ℕ)
25
 
 
26
 
  zero : ℕ
27
 
  zero = inj₁ _
28
 
 
29
 
  suc : ℕ → ℕ
30
 
  suc n = inj₂ (fold n)
31
 
 
32
 
  ℕ-rec : (P : ℕ → Set) →
33
 
          P zero →
34
 
          (∀ n → P n → P (suc n)) →
35
 
          ∀ n → P n
36
 
  ℕ-rec P z s (inj₁ _)        = z
37
 
  ℕ-rec P z s (inj₂ (fold n)) = s n (ℕ-rec P z s n)
38
 
 
39
 
module ℕ₂ where
40
 
 
41
 
  data ℕC : Set where
42
 
    ′zero : ℕC
43
 
    ′suc  : ℕC
44
 
 
45
 
  mutual
46
 
 
47
 
    ℕ : Set
48
 
    ℕ = ∃ λ (c : ℕC) → ℕ′ c
49
 
 
50
 
    ℕ′ : ℕC → Set
51
 
    ℕ′ ′zero = ⊤
52
 
    ℕ′ ′suc  = Rec (♯ ℕ)
53
 
 
54
 
  zero : ℕ
55
 
  zero = (′zero , _)
56
 
 
57
 
  suc : ℕ → ℕ
58
 
  suc n = (′suc , fold n)
59
 
 
60
 
  ℕ-rec : (P : ℕ → Set) →
61
 
          P zero →
62
 
          (∀ n → P n → P (suc n)) →
63
 
          ∀ n → P n
64
 
  ℕ-rec P z s (′zero , _)      = z
65
 
  ℕ-rec P z s (′suc  , fold n) = s n (ℕ-rec P z s n)