← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/prototyping/modules/flat/test.mod

  • 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:
src/prototyping/modules/flat/test.mod
1
 
 
2
 
module Top where
3
 
 
4
 
  Nat  : Set
5
 
  zero : Nat
6
 
  suc  : Nat -> Nat
7
 
  plus : Nat -> Nat -> Nat
8
 
 
9
 
  module Test1 where
10
 
 
11
 
    module A where
12
 
      z : Nat = suc (suc zero)
13
 
    module B where
14
 
      module C where
15
 
        x : Nat = suc zero
16
 
      open C
17
 
      open A
18
 
      y : Nat = zero
19
 
    module D = B
20
 
 
21
 
  module Test2 where
22
 
 
23
 
    module Q where
24
 
      module R where
25
 
        f : Nat -> Nat = \x -> zero
26
 
 
27
 
    module B (n : Nat) where
28
 
      open Q.R public
29
 
      q : Nat = n
30
 
 
31
 
    n : Nat = B.f zero zero
32
 
 
33
 
    module Bz = B zero renaming (q to r)
34
 
 
35
 
    m : Nat = Bz.f zero
36
 
 
37
 
  module Test3 where
38
 
    module B (n : Nat) where
39
 
      module C (m : Nat) where
40
 
        q : Nat = m
41
 
      z : Nat = zero
42
 
 
43
 
    module D = B zero renaming (module C to C')
44
 
    module E = D.C' (suc zero) renaming (q to m')
45
 
 
46
 
    q : Nat = E.m'
47
 
 
48
 
  module Test4 where
49
 
 
50
 
    module B (n : Nat) where
51
 
      m : Nat = n
52
 
 
53
 
    module Z = B zero
54
 
 
55
 
    z : Nat = Z.m
56
 
 
57
 
    module C where
58
 
      f : Nat -> Nat
59
 
 
60
 
    module D where
61
 
      open C
62
 
      g : Nat -> Nat = f
63
 
 
64
 
    module Ind (P : Nat -> Set) where
65
 
 
66
 
      base : P zero
67
 
      step : (n : Nat) -> P n -> P (suc n)
68
 
 
69
 
    module Id (A : Set) where
70
 
 
71
 
      id : A -> A = \x -> x
72
 
 
73
 
      module Foo (x : A) where
74
 
        const : (B : Set) -> B -> A
75
 
              = \B -> \b -> x
76
 
 
77
 
    module NatId = Id Nat
78
 
 
79
 
    module Q where
80
 
      module Foo' (X : Set)(x : X) = Id.Foo X x
81
 
 
82
 
    open NatId
83
 
 
84
 
    z : Nat = id zero
85
 
 
86
 
  module Test5 where
87
 
 
88
 
    f (n : Nat) : Nat = x
89
 
      where
90
 
        x : Nat = n
91
 
 
92
 
  module Test6 where
93
 
 
94
 
    module A (n : Nat) where
95
 
      x : Nat = n
96
 
      y : Nat = x
97
 
 
98
 
    module B (m : Nat)(p : Nat) = A (plus m p)
99
 
 
100
 
    module C (m : Nat) where
101
 
      z : Nat = m
102
 
      module A' (p : Nat) = A (plus p z)
103
 
      foo : Nat = A'.y zero
104
 
 
105
 
  module Test7 where
106
 
 
107
 
    f (n : Nat) : Nat = x
108
 
      where
109
 
        module A where
110
 
          x : Nat = n
111
 
        open A public
112
 
 
113
 
  module Test8 where
114
 
 
115
 
    f (n : Nat) : Nat = x
116
 
      module f where
117
 
        x : Nat = n
118
 
 
119
 
    y : Nat = f.x zero
120
 
 
121
 
    g (n : Nat) : Nat = z n
122
 
      module g (m : Nat) where
123
 
        z : Nat = plus n m
124
 
 
125
 
    z : Nat = g.z zero zero
126