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

diff zf.agda @ 51:83b13f1f4f42

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 Mon, 27 May 2019 15:00:45 +0900
parents f10ceee99d00
children 33fb8228ace9
line wrap: on
line diff
--- a/zf.agda	Sat May 25 21:31:07 2019 +0900
+++ b/zf.agda	Mon May 27 15:00:45 2019 +0900
@@ -57,9 +57,9 @@
   _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set m
   _⊆_ A B {x} = A ∋ x →  B ∋ x
   _∩_ : ( A B : ZFSet  ) → ZFSet
-  A ∩ B = Select (A , B) (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
+  A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
   _∪_ : ( A B : ZFSet  ) → ZFSet
-  A ∪ B = Select (A , B) (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  )
+  A ∪ B = Union (A , B) 
   infixr  200 _∈_
   infixr  230 _∩_ _∪_
   infixr  220 _⊆_