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

diff src/ordinal.agda @ 1298:2c34f2b554cf current

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Replace and filter projection fix done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 03 Jun 2023 17:31:17 +0900
parents 7c39cae23803
children 47d3cc596d68
line wrap: on
line diff
--- a/src/ordinal.agda	Sat Jun 03 08:13:50 2023 +0900
+++ b/src/ordinal.agda	Sat Jun 03 17:31:17 2023 +0900
@@ -250,7 +250,7 @@
    isNext = record {
         x<nx = x<nx 
       ; osuc<nx = λ {x} {y} → osuc<nx {x} {y}
-      ; ¬nx<nx = ¬nx<nx 
+      -- ; ¬nx<nx = ¬nx<nx 
    }
   } where
      next : Ordinal {suc n} → Ordinal {suc n}