Mercurial > hg > Members > atton > agda-proofs
annotate systemT/systemT.agda @ 59:352e8a724829
Trying define maybe-subtype......
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 12 Jan 2017 02:48:09 +0000 (2017-01-12) |
parents | fe247f476ecb |
children |
rev | line source |
---|---|
1
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 module systemT where |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 data Bool : Set where |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 T : Bool |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 F : Bool |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 data Int : Set where |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 O : Int |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 S : Int -> Int |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 R : {U : Set} -> U -> (U -> (Int -> U)) -> Int -> U |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 R u v O = u |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 R u v (S t) = v (R u v t) t |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 D : {U : Set} -> U -> U -> Bool -> U |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 D u v F = v |
fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 D u v T = u |