Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ODC.agda @ 369:17adeeee0c2a
fix Select and Replace
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 19 Jul 2020 10:02:43 +0900 |
parents | 7f919d6b045b |
children | 1425104bb5d8 |
line wrap: on
line diff
--- a/ODC.agda Sun Jul 19 03:24:39 2020 +0900 +++ b/ODC.agda Sun Jul 19 10:02:43 2020 +0900 @@ -1,3 +1,4 @@ +{-# OPTIONS --allow-unsolved-metas #-} open import Level open import Ordinals module ODC {n : Level } (O : Ordinals {n} ) where @@ -87,12 +88,12 @@ ; _∋_ = _∋_ ; _≈_ = _=h=_ ; ∅ = od∅ - ; Select = Select + ; Select = {!!} ; isZFC = isZFC } where -- infixr 200 _∈_ -- infixr 230 _∩_ _∪_ - isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select + isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ {!!} isZFC = record { choice-func = choice-func ; choice = choice