Mercurial > hg > Members > atton > agda > systemF

comparison systemF.agda @ 20:de9e05b25acf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define List
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 10 Apr 2014 14:29:37 +0900
parents 9eb6fcf6fc7d
children 25b62c46081b
comparison
equal deleted inserted replaced
19:9eb6fcf6fc7d 20:de9e05b25acf
132 132
133 -- Proofs And Types Style lemma-R-n 133 -- Proofs And Types Style lemma-R-n
134 -- lemma-R-n : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} {n : Int} -> R u f (S n) ≡ f (R u f n) n 134 -- lemma-R-n : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} {n : Int} -> R u f (S n) ≡ f (R u f n) n
135 -- n in (S n) and (R u f n) has (U × Int), but last n has Int. 135 -- n in (S n) and (R u f n) has (U × Int), but last n has Int.
136 -- regenerate same (n : Int) by used g, <_,_> 136 -- regenerate same (n : Int) by used g, <_,_>
137 -- NOTE : Proofs And Types say "equation for recursion is satisfied by values only"
137 138
138 139
140 -- List
139 141
142 List : {l : Level} -> (U : Set l) -> Set (suc l)
143 List {l} U = {X : Set l} -> X -> (U -> X -> X) -> X
144
145 nil : {l : Level} {U : Set l} -> List U
146 nil {l} {U} = \{X : Set l} -> \(x : X) -> \(y : U -> X -> X) -> x
147
148 cons : {l : Level} {U : Set l} -> U -> List U -> List U
149 cons {l} {U} u t = \{X : Set l} -> \(x : X) -> \(y : U -> X -> X) -> y u (t {X} x y)
150
151 ListIt : {l : Level} {U W : Set l} -> W -> (U -> W -> W) -> List U -> W
152 ListIt {l} {U} {W} w f t = t {W} w f
153
154 lemma-list-it-nil : {l : Level} {U W : Set l} {w : W} {f : U -> W -> W} -> ListIt w f nil ≡ w
155 lemma-list-it-nil = refl
156
157 lemma-list-it-cons : {l : Level} {U W : Set l} {u : U} {w : W} {f : U -> W -> W} {t : List U} -> ListIt w f (cons u t) ≡ f u (ListIt w f t)
158 lemma-list-it-cons = refl