Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 33:2b853472cb24
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 21 May 2019 18:17:24 +0900 |
| parents | 3b0fdb95618e |
| children | c9ad0d97ce41 |
| files | ordinal-definable.agda ordinal.agda |
| diffstat | 2 files changed, 1 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/ordinal-definable.agda Tue May 21 00:30:01 2019 +0900 +++ b/ordinal-definable.agda Tue May 21 18:17:24 2019 +0900 @@ -96,6 +96,7 @@ c3 lx (Φ .lx) d not | t | () c3 lx (OSuc .lx x₁) d not with not ( record { lv = lx ; ord = OSuc lx x₁ } ) ... | t with t (case2 (s< {!!} ) ) +-- x d< OSuc lx x is bad on ℵ case c3 lx (OSuc .lx x₁) d not | t | () c3 .(Suc lv) (ℵ lv) not = {!!}
--- a/ordinal.agda Tue May 21 00:30:01 2019 +0900 +++ b/ordinal.agda Tue May 21 18:17:24 2019 +0900 @@ -36,16 +36,6 @@ open import Relation.Binary open import Relation.Binary.Core -¬ℵ : {n : Level} {lx : Nat } ( x : OrdinalD {n} lx ) → Set -¬ℵ (Φ lv₁) = ⊤ -¬ℵ (OSuc lv₁ x) = ¬ℵ x -¬ℵ (ℵ lv₁) = ⊥ - -s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → ¬ℵ x → x d< OSuc lx x -s<refl {n} {.lv₁} {Φ lv₁} t = Φ< -s<refl {n} {.lv₁} {OSuc lv₁ x} t = s< (s<refl t) -s<refl {n} {.(Suc lv₁)} {ℵ lv₁} () - o∅ : {n : Level} → Ordinal {n} o∅ = record { lv = Zero ; ord = Φ Zero }