### view systemF/int.agda @ 77:a2e6f61d5f2bdefaulttip

author atton Thu, 09 Feb 2017 06:32:03 +0000 4c1a6ce23f9e
line wrap: on
line source
```
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 : {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 = \z -> \s -> (R (R z (\x -> \_ -> s x) a) (\x -> \_ -> s x) b)

lemma-same-add : {l : Level} {U : Set l} -> add ≡ add-r {_} {U}