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

diff filter.agda @ 301:b012a915bbb5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
contradiction found ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 24 Jun 2020 14:05:38 +0900
parents e70980bd80c7
children 5544f4921a44
line wrap: on
line diff
--- a/filter.agda	Tue Jun 23 15:12:43 2020 +0900
+++ b/filter.agda	Wed Jun 24 14:05:38 2020 +0900
@@ -129,9 +129,11 @@
 
 --    the set of finite partial functions from ω to 2
 --
+--   ph2 : Nat → Set → 2
+--   ph2 : Nat → Maybe 2
+--
 -- Hω2 : Filter (Power (Power infinite))
 
-
 record Ideal  ( L : OD  ) : Set (suc n) where
    field
        ideal : OD