Mercurial > hg > Members > atton > agda > systemT
changeset 1:f300bd2101d3
Define Bool, Int, D and R
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 09 May 2014 13:03:29 +0900 |
parents | c9c65ee9e9f9 |
children | ca2e9f7a7898 |
files | systemT.agda |
diffstat | 1 files changed, 17 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/systemT.agda Fri May 09 13:03:29 2014 +0900 @@ -0,0 +1,17 @@ +module systemT where + +data Bool : Set where + T : Bool + F : Bool + +data Int : Set where + O : Int + S : Int -> Int + +R : {U : Set} -> U -> (U -> (Int -> U)) -> Int -> U +R u v O = u +R u v (S t) = v (R u v t) t + +D : {U : Set} -> U -> U -> Bool -> U +D u v F = v +D u v T = u