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

diff zf.agda @ 236:650bdad56729

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 16 Aug 2019 15:53:29 +0900
parents 2e1f19c949dc
children d09437fcfc7c
line wrap: on
line diff
--- a/zf.agda	Thu Aug 15 04:51:24 2019 +0900
+++ b/zf.agda	Fri Aug 16 15:53:29 2019 +0900
@@ -34,7 +34,7 @@
   _∩_ : ( A B : ZFSet  ) → ZFSet
   A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
   _∪_ : ( A B : ZFSet  ) → ZFSet
-  A ∪ B = Union (A , B)    -- Select A (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  ) is easer
+  A ∪ B = Union (A , B)    -- Select A (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  ) is easier
   ｛_｝ : ZFSet → ZFSet
   ｛ x ｝ = ( x ,  x )
   infixr  200 _∈_