X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fdatatypes%2Fbool.ma;fp=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fdatatypes%2Fbool.ma;h=eda979d69b3c1121e76dadec86b5c789f8559086;hb=4b940bfbeab1181dd18c56e46761f5e6690d9f9d;hp=be42b597a5abd471a2000a85272ecb12d50d06fe;hpb=90ff94e74ceed0954b8599bff55d5c84f15c1b9f;p=helm.git

diff --git a/helm/software/matita/nlibrary/datatypes/bool.ma b/helm/software/matita/nlibrary/datatypes/bool.ma
index be42b597a..eda979d69 100644
--- a/helm/software/matita/nlibrary/datatypes/bool.ma
+++ b/helm/software/matita/nlibrary/datatypes/bool.ma
@@ -14,6 +14,9 @@
 
 include "logic/pts.ma".
 
-ninductive bool: Type[0] ≝
-   true: bool
- | false: bool.
\ No newline at end of file
+ninductive bool: Type[0] ≝ true: bool | false: bool.
+ 
+ndefinition orb ≝ λa,b:bool. match a with [ true ⇒ true | _ ⇒ b ].
+
+notation "a || b" left associative with precedence 30 for @{'orb $a $b}.
+interpretation "orb" 'orb a b = (orb a b).
\ No newline at end of file