Mercurial > hg > Members > atton > agda > systemF
changeset 13:4977c5873660
Add lemma-it of Int, but has yellow
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 08 Apr 2014 16:31:08 +0900 |
| parents | 627da4867e5b |
| children | 491a08669724 |
| files | systemF.agda |
| diffstat | 1 files changed, 6 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/systemF.agda Tue Apr 08 15:29:46 2014 +0900 +++ b/systemF.agda Tue Apr 08 16:31:08 2014 +0900 @@ -93,10 +93,10 @@ -- Int -Int : {l : Level} {X : Set l} -> Set l +Int : {l : Level} -> {X : Set l} -> Set l Int {l} {X} = X -> (X -> X) -> X -O : {l : Level} -> {X : Set l} -> Int +O : {l : Level} -> {X : Set l} -> Int O {l} {X} = \(x : X) -> \(y : X -> X) -> x S : {l : Level} -> {X : Set l} -> Int -> Int @@ -112,4 +112,7 @@ lemma-it-s-o = refl g : {l : Level} -> {U : Set l} -> {f : U -> Int {l} {U} -> U} -> (U × Int) -> (U × Int) -g {l} {U} {f} = \x -> < (f (π1 x) (π2 x)) , S (π2 x) > \ No newline at end of file +g {l} {U} {f} = \x -> < (f (π1 x) (π2 x)) , S (π2 x) > + +lemma-it : {l : Level} {U : Set l} {u : U} {n : Int} {f : U -> Int -> U} -> g {l} {U} {f} < u , n > ≡ < f u n , S n > +lemma-it = refl