← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test/succeed/Issue154.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/succeed/Issue154.agda
1
 
module Issue154 where
2
 
 
3
 
module A where
4
 
  postulate X : Set
5
 
 
6
 
module B where
7
 
  postulate X : Set
8
 
 
9
 
  module C where
10
 
    open A public
11
 
    -- X is ambiguous here, but only exported once from C
12
 
 
13
 
module D where
14
 
  private postulate X : Set
15
 
  open A public
16
 
  -- same here
17
 
 
18
 
module E where
19
 
  postulate X : Set
20
 
  open A
21
 
  -- and here
22
 
 
23
 
module F where
24
 
  open A public
25
 
  open D public
26
 
  -- in this case there is no ambiguity, A.X and D.X refer
27
 
  -- to the same entity (A.X)
28
 
 
29
 
module G where
30
 
  open B public
31
 
 
32
 
module H where
33
 
  open G public
34
 
  open B public
35
 
  -- same as F but for modules
36
 
 
37
 
postulate
38
 
  test : A.X → B.X → B.C.X → D.X → E.X → F.X → G.X → H.X