Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal.agda @ 218:eee983e4b402
try func
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 06 Aug 2019 15:50:14 +0900 |
| parents | 22d435172d1a |
| children | 95a26d1698f4 |
line wrap: on
line diff
--- a/ordinal.agda Mon Aug 05 17:02:37 2019 +0900 +++ b/ordinal.agda Tue Aug 06 15:50:14 2019 +0900 @@ -29,6 +29,12 @@ _o<_ : {n : Level} ( x y : Ordinal ) → Set n _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y ) +o<-dom : {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal +o<-dom {n} {x} _ = x + +o<-cod : {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal +o<-cod {n} {_} {y} _ = y + s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x s<refl {n} {lv} {Φ lv} = Φ< s<refl {n} {lv} {OSuc lv x} = s< s<refl