Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison filter.agda @ 276:6f10c47e4e7a
separate choice
fix sup-o
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 09 May 2020 09:02:52 +0900 |
parents | 985a1af11bce |
children | d9d3654baee1 |
comparison
equal
deleted
inserted
replaced
275:455792eaa611 | 276:6f10c47e4e7a |
---|---|
79 | 79 |
80 module in-countable-ordinal {n : Level} where | 80 module in-countable-ordinal {n : Level} where |
81 | 81 |
82 import ordinal | 82 import ordinal |
83 | 83 |
84 open ordinal.C-Ordinal-with-choice | 84 -- open ordinal.C-Ordinal-with-choice |
85 | 85 |
86 Hω2 : Filter (Power (Power infinite)) | 86 Hω2 : Filter (Power (Power infinite)) |
87 Hω2 = {!!} | 87 Hω2 = {!!} |
88 | 88 |