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

diff ordinal.agda @ 325:1a54dbe1ea4c

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 Sat, 04 Jul 2020 22:48:49 +0900
parents fbabb20f222e
children 5544f4921a44
line wrap: on
line diff
--- a/ordinal.agda	Sat Jul 04 18:18:17 2020 +0900
+++ b/ordinal.agda	Sat Jul 04 22:48:49 2020 +0900
@@ -211,7 +211,7 @@
    ; o∅ = o∅
    ; osuc = osuc
    ; _o<_ = _o<_
-   ; next = ?
+   ; next = {!!}
    ; isOrdinal = record {
        Otrans = ordtrans
      ; OTri = trio<
@@ -219,8 +219,8 @@
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<
      ; TransFinite = TransFinite1
-     ; is-limit = ?
-     ; next-limit = ?
+     ; is-limit = {!!}
+     ; next-limit = {!!}
    }
   } where
      ord1 : Set (suc n)