Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff LEMC.agda @ 370:1425104bb5d8
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 19 Jul 2020 12:26:17 +0900 |
parents | 17adeeee0c2a |
children | 6c72bee25653 |
line wrap: on
line diff
--- a/LEMC.agda Sun Jul 19 10:02:43 2020 +0900 +++ b/LEMC.agda Sun Jul 19 12:26:17 2020 +0900 @@ -40,12 +40,12 @@ ; _∋_ = _∋_ ; _≈_ = _=h=_ ; ∅ = od∅ - ; Select = ? + ; Select = {!!} ; isZFC = isZFC } where -- infixr 200 _∈_ -- infixr 230 _∩_ _∪_ - isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ ? + isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ {!!} isZFC = record { choice-func = λ A {X} not A∋X → a-choice (choice-func X not ); choice = λ A {X} A∋X not → is-in (choice-func X not)