← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test/succeed/Issue435.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/Issue435.agda
1
 
 
2
 
module Issue435 where
3
 
 
4
 
data Bool : Set where
5
 
  true false : Bool
6
 
 
7
 
record Unit : Set where
8
 
 
9
 
postulate
10
 
  Dh : ({ x : Bool } → Bool) → Set
11
 
  Di : ({{x : Bool}} → Bool) → Set
12
 
 
13
 
noth : Set
14
 
noth = Dh (\ { {true}  → false ; {false} → true})
15
 
 
16
 
noti : Set
17
 
noti = Di (\ { {{true}}  → false ; {{false}} → true})
18
 
 
19
 
 
20
 
data ⊥ : Set where
21
 
 
22
 
data T : Set where
23
 
  expl : (⊥ → ⊥) → T
24
 
  impl : ({_ : ⊥} → ⊥) → T
25
 
  inst : ({{_ : ⊥}} → ⊥) → T
26
 
 
27
 
explicit : T
28
 
explicit = expl (λ ())
29
 
 
30
 
implicit : T
31
 
implicit = impl (λ {})
32
 
 
33
 
instance : T
34
 
instance = inst (λ {{ }})
35
 
 
36
 
explicit-match : T
37
 
explicit-match = expl (λ { () })
38
 
 
39
 
implicit-match : T
40
 
implicit-match = impl (λ { {} })
41
 
 
42
 
implicit-match′ : T
43
 
implicit-match′ = impl (λ { { () } })
44
 
 
45
 
instance-match : T
46
 
instance-match = inst (λ { {{}} })
47
 
 
48
 
instance-match′ : T
49
 
instance-match′ = inst (λ { {{ () }} })