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

comparison Ordinals.agda @ 256:6e1c60866788 release

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
orderd pair and product
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 29 Aug 2019 16:18:37 +0900
parents 846e0926bb89
children 63df67b6281c
comparison
equal deleted inserted replaced
232:fe8392f527eb 256:6e1c60866788
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