Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff BAlgbra.agda @ 360:2a8a51375e49
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 15 Jul 2020 08:42:30 +0900 |
| parents | 12071f79f3cf |
| children | 17adeeee0c2a |
line wrap: on
line diff
--- a/BAlgbra.agda Tue Jul 14 15:02:59 2020 +0900 +++ b/BAlgbra.agda Wed Jul 15 08:42:30 2020 +0900 @@ -25,9 +25,9 @@ open _∨_ open Bool -_∩_ : ( A B : HOD ) → HOD -A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; - odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y)) } +--_∩_ : ( A B : HOD ) → HOD +--A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; +-- odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y)) } _∪_ : ( A B : HOD ) → HOD A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;