Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison filter.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 | 5de8905a5a2b 359402cc6c3d |
comparison
equal
deleted
inserted
replaced
276:6f10c47e4e7a | 277:d9d3654baee1 |
---|---|
15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) | 15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
16 | 16 |
17 open inOrdinal O | 17 open inOrdinal O |
18 open OD O | 18 open OD O |
19 open OD.OD | 19 open OD.OD |
20 open ODAxiom odAxiom | |
20 | 21 |
21 open _∧_ | 22 open _∧_ |
22 open _∨_ | 23 open _∨_ |
23 open Bool | 24 open Bool |
24 | 25 |