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

diff src/LEMC.agda @ 440:d1c9f5ae5d0a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
give up this generic filter definition
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 01 Mar 2022 14:31:31 +0900
parents a5f8084b8368
children 55ab5de1ae02
line wrap: on
line diff
--- a/src/LEMC.agda	Sat Feb 26 17:44:30 2022 +0900
+++ b/src/LEMC.agda	Tue Mar 01 14:31:31 2022 +0900
@@ -131,7 +131,6 @@
          --
          --  from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only
          --
-         -- FIXME : don't use HOD make this level n, so we can remove ε-induction1 
          record Minimal (x : HOD)  : Set (suc n) where
            field
                min : HOD