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

changeset 305:4804f3f3485f

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 Mon, 29 Jun 2020 18:37:31 +0900
parents 2c111bfcc89a
children b07fc3ef5aab
files OD.agda
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Mon Jun 29 18:31:56 2020 +0900
+++ b/OD.agda	Mon Jun 29 18:37:31 2020 +0900
@@ -147,7 +147,7 @@
 x c< a = a ∋ x 
 
 cseq : {n : Level} →  HOD  →  HOD 
-cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = {!!} ; <odmax = {!!} } where
+cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = ? } where
 
 odef-subst :  {Z : HOD } {X : Ordinal  }{z : HOD } {x : Ordinal  }→ odef Z X → Z ≡ z  →  X ≡ x  →  odef z x
 odef-subst df refl refl = df