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

comparison Ordinals.agda @ 235:846e0926bb89

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix cardinal
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 15 Aug 2019 04:51:24 +0900
parents 59771eb07df0
children 63df67b6281c
comparison
equal deleted inserted replaced
234:e06b76e5b682 235:846e0926bb89
48 o∅ = Ordinals.o∅ O 48 o∅ = Ordinals.o∅ O
49 49
50 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O) 50 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
51 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O) 51 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O)
52 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O) 52 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O)
53 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O)
53 54
54 o<-dom : { x y : Ordinal } → x o< y → Ordinal 55 o<-dom : { x y : Ordinal } → x o< y → Ordinal
55 o<-dom {x} _ = x 56 o<-dom {x} _ = x
56 57
57 o<-cod : { x y : Ordinal } → x o< y → Ordinal 58 o<-cod : { x y : Ordinal } → x o< y → Ordinal