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

changeset 1450:b7f6eb9eaf0d

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 Wed, 05 Jul 2023 12:35:36 +0900
parents a295c52af3b7
children 682fe6b32b2a
files src/cardinal.agda
diffstat 1 files changed, 2 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Wed Jul 05 10:57:43 2023 +0900
+++ b/src/cardinal.agda	Wed Jul 05 12:35:36 2023 +0900
@@ -373,13 +373,14 @@
 
      p0 : odef (Power S) o∅
      p0 z xz = ⊥-elim (¬x<0 (subst (λ k → odef k z) o∅≡od∅ xz)  )
-
+ 
      s : Ordinal 
      s = fun→ b o∅ p0
 
      ss : odef S s
      ss = funB b o∅ p0
 
+
      diag4 : ⊥ 
      diag4 with ODC.p∨¬p O ( odef (* (fun← b s ss)) s)
      ... | case1 y  = ?