# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1398652209 -32400
# Node ID 7b0f2025112bb02ff8e1f059f5dae2186c73c5f7
# Parent  852798763d56ef3d4b90606239f4bc83955b4d43
Define Add on Int

diff -r 852798763d56 -r 7b0f2025112b int.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/int.agda	Mon Apr 28 11:30:09 2014 +0900
@@ -0,0 +1,58 @@
+module int where
+
+open import Relation.Binary.PropositionalEquality
+open import Level
+open import systemF
+
+-- define values
+
+one : {l : Level} {U : Set l} -> Int {l} {U}
+one = S O
+
+two : {l : Level} {U : Set l} -> Int {l} {U}
+two = S (S O)
+
+three : {l : Level} {U : Set l} -> Int {l} {U}
+three = S (S (S O))
+
+four : {l : Level} {U : Set l} -> Int {l} {U}
+four = S (S (S (S O)))
+
+five : {l : Level} {U : Set l} -> Int {l} {U}
+five = S (S (S (S (S O))))
+
+six : {l : Level} {U : Set l} -> Int {l} {U}
+six =  S (S (S (S (S (S O)))))
+
+seven : {l : Level} {U : Set l} -> Int {l} {U}
+seven = S (S (S (S (S (S (S O))))))
+
+eight : {l : Level} {U : Set l} -> Int {l} {U}
+eight = S (S (S (S (S (S (S (S O)))))))
+
+nine : {l : Level} {U : Set l} -> Int {l} {U}
+nine = S (S (S (S (S (S (S (S (S O))))))))
+
+ten : {l : Level} {U : Set l} -> Int {l} {U}
+ten = S (S (S (S (S (S (S (S (S O))))))))
+
+
+-- add
+
+add : {l : Level} {U : Set l} -> Int -> Int -> Int
+add {l} {U} a b = \(x : U) -> \(y : (U -> U)) -> a (b x y) y
+
+add-r : {l : Level} {U : Set l} -> Int -> Int -> Int
+add-r {l} {U} a b = R a (\x -> \n -> S x) b
+
+lemma-same-add : {l : Level} {U : Set l} -> add ≡ add-r {l} {U}
+lemma-same-add = refl
+
+lemma-add-zero-zero : {l : Level} {U : Set l} -> add O O ≡ O {_} {U}
+lemma-add-zero-zero = refl
+
+lemma-add-one-two : {l : Level} {U : Set l} -> add one two ≡ three {_} {U}
+lemma-add-one-two = refl
+
+--lemma-add-swap : {l : Level} {U : Set l} {a b : Int}  -> add a b ≡ add b a
+--lemma-add-swap = refl
diff -r 852798763d56 -r 7b0f2025112b systemF.agda
--- a/systemF.agda	Tue Apr 22 11:11:50 2014 +0900
+++ b/systemF.agda	Mon Apr 28 11:30:09 2014 +0900
@@ -213,3 +213,5 @@
 
 lemma-tree-it-collect : {l : Level} {U W : Set l} {w : W} {h : (U -> W) -> W} {f : U -> Tree U} -> (TreeIt w h (collect f)) ≡ (h (\(x : U) -> TreeIt w h (f x)))
 lemma-tree-it-collect = refl
+
+