Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison ordinal.agda @ 325:1a54dbe1ea4c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 04 Jul 2020 22:48:49 +0900
parents fbabb20f222e
children 5544f4921a44
comparison
equal deleted inserted replaced
324:fbabb20f222e 325:1a54dbe1ea4c
209 C-Ordinal {n} = record { 209 C-Ordinal {n} = record {
210 ord = Ordinal {suc n} 210 ord = Ordinal {suc n}
211 ; o∅ = o∅ 211 ; o∅ = o∅
212 ; osuc = osuc 212 ; osuc = osuc
213 ; _o<_ = _o<_ 213 ; _o<_ = _o<_
214 ; next = ? 214 ; next = {!!}
215 ; isOrdinal = record { 215 ; isOrdinal = record {
216 Otrans = ordtrans 216 Otrans = ordtrans
217 ; OTri = trio< 217 ; OTri = trio<
218 ; ¬x<0 = ¬x<0 218 ; ¬x<0 = ¬x<0
219 ; <-osuc = <-osuc 219 ; <-osuc = <-osuc
220 ; osuc-≡< = osuc-≡< 220 ; osuc-≡< = osuc-≡<
221 ; TransFinite = TransFinite1 221 ; TransFinite = TransFinite1
222 ; is-limit = ? 222 ; is-limit = {!!}
223 ; next-limit = ? 223 ; next-limit = {!!}
224 } 224 }
225 } where 225 } where
226 ord1 : Set (suc n) 226 ord1 : Set (suc n)
227 ord1 = Ordinal {suc n} 227 ord1 = Ordinal {suc n}
228 TransFinite1 : { ψ : ord1 → Set (suc n) } 228 TransFinite1 : { ψ : ord1 → Set (suc n) }