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

diff Todo @ 1283:f4dac8be0a01

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 Sat, 13 May 2023 10:53:32 +0900
parents 9984cdd88da3
children 171c3f3cdc6b
line wrap: on
line diff
--- a/Todo	Thu Apr 06 15:32:29 2023 +0900
+++ b/Todo	Sat May 13 10:53:32 2023 +0900
@@ -1,3 +1,8 @@
+Sat May 13 10:51:35 JST 2023
+
+    use Filter (ZFP (Proj1 (ZFP PQ)) (Proj2 (ZFP PQ)) for projection of Ultra filter
+    tranfinite induciton on well-founded set
+
 Sat Aug  1 13:16:53 JST 2020
 
     P Generic Filter