Mercurial > hg > Members > atton > agda > systemF

changeset 11:60151a653141

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add comment
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 08 Apr 2014 13:34:26 +0900
parents 49721ad2f556
children 627da4867e5b
files systemF.agda
diffstat 1 files changed, 3 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/systemF.agda	Tue Apr 08 13:31:25 2014 +0900
+++ b/systemF.agda	Tue Apr 08 13:34:26 2014 +0900
@@ -111,5 +111,6 @@
 lemma-it-s-o : {U : Set l} -> {u : U} -> {f : U -> U} -> {t : Int} -> It u f (S t) ≡ f (It u f t)
 lemma-it-s-o = refl
 
-g : {l : Level} -> {U : Set (suc l)} -> {f : U -> Int -> U} -> (U × Int) -> (_×_ {suc l} {suc l} U Int)
-g {l} {U} {f} = \x -> \{X : Set l} -> <_,_> {suc l} {suc l} {l} {U} {Int} (f (π1 x) (π2 x)) (π2 x)
\ No newline at end of file
+g : {l : Level} -> {U : Set (suc l)} -> {f : U -> Int -> U} -> (U × Int) -> (U × Int)
+g {l} {U} {f} = \x -> \{X : Set l} -> <_,_> {suc l} {suc l} {l} {U} {Int} (f (π1 x) (π2 x)) (π2 x)
+-- g {l} {U} {f} = \x -> < (f (π1 x) (π2 x)) , (π2 x) > -- {X} in _×_ removed by applied U. add \{X} lambda to type checking
\ No newline at end of file