Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison cardinal.agda @ 277:d9d3654baee1
seperate choice from LEM
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 09 May 2020 09:38:21 +0900 |
parents | 6f10c47e4e7a |
children | 12071f79f3cf |
comparison
equal
deleted
inserted
replaced
276:6f10c47e4e7a | 277:d9d3654baee1 |
---|---|
17 | 17 |
18 open inOrdinal O | 18 open inOrdinal O |
19 open OD O | 19 open OD O |
20 open OD.OD | 20 open OD.OD |
21 open OPair O | 21 open OPair O |
22 open ODAxiom odAxiom | |
22 | 23 |
23 open _∧_ | 24 open _∧_ |
24 open _∨_ | 25 open _∨_ |
25 open Bool | 26 open Bool |
26 open _==_ | 27 open _==_ |