setoids.ma split into setoids.ma + setoids1.ma

[helm.git] / helm / software / matita / nlibrary / logic / connectives.ma

diff --git a/helm/software/matita/nlibrary/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma
index 02002dc834a31081c97b26c30cbeb5102ae2f7fe..026e9216951c9224737b6493953317effd635369 100644 (file)
--- a/helm/software/matita/nlibrary/logic/connectives.ma
+++ b/helm/software/matita/nlibrary/logic/connectives.ma
@@ -38,4 +38,19 @@ interpretation "logical or" 'or x y = (Or x y).
 ninductive Ex (A:Type) (P:A → CProp) : CProp ≝
     ex_intro: ∀x:A. P x → Ex A P.
 
-interpretation "exists" 'exists x = (Ex ? x).
\ No newline at end of file
+interpretation "exists" 'exists x = (Ex ? x).
+
+nrecord iff (A,B: CProp) : CProp ≝
+ { if: A → B;
+   fi: B → A
+ }.
+
+notation > "hvbox(a break \liff b)"
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+notation "hvbox(a break \leftrightarrow b)"
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+interpretation "logical iff" 'iff x y = (iff x y).