Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff LEMC.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/LEMC.agda Sun Jul 19 03:24:39 2020 +0900 +++ b/LEMC.agda Sun Jul 19 10:02:43 2020 +0900 @@ -40,12 +40,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 = λ A {X} not A∋X → a-choice (choice-func X not ); choice = λ A {X} A∋X not → is-in (choice-func X not)