← Back to branch summary

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

« back to all changes in this revision

Viewing changes to notes/papers/implicit/examples/Dangerous-Agda1.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:
notes/papers/implicit/examples/Dangerous-Agda1.agda
1
 
 
2
 
data N : Set = zero | suc (n:N)
3
 
data B : Set = true | false
4
 
 
5
 
data False : Set =
6
 
data True  : Set = tt
7
 
 
8
 
F : B -> Set
9
 
F true  = N
10
 
F false = B
11
 
 
12
 
G : (x:B) -> F x -> Set
13
 
G false _      = N
14
 
G true zero    = B
15
 
G true (suc n) = N
16
 
 
17
 
(==) : B -> B -> Set
18
 
true == true = True
19
 
false == false = True
20
 
_ == _ = False
21
 
 
22
 
data Equal (x,y:B) : Set where
23
 
  equal : x == y -> Equal x y
24
 
 
25
 
refl : (x:B) -> Equal x x
26
 
refl true = equal tt
27
 
refl false = equal tt
28
 
 
29
 
postulate
30
 
  f : (x:B) -> (y : F x) -> G x y -> N -- Equal x true -> N
31
 
 
32
 
h : N
33
 
h = f _ false zero --(refl true)
34