]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/ng_assembly2/num/bool.ma
mod change (-x)
[helm.git] / helm / software / matita / contribs / ng_assembly2 / num / bool.ma
old mode 100755 (executable)
new mode 100644 (file)
index 8092713..8d97483
@@ -31,7 +31,6 @@ ninductive bool : Type ≝
 | false : bool.
 
 (* operatori booleani *)
-
 ndefinition eq_bool ≝
 λb1,b2:bool.match b1 with
  [ true ⇒ match b2 with [ true ⇒ true | false ⇒ false ]
@@ -74,5 +73,8 @@ notation "hvbox(a break ⊙ b)" left associative with precedence 33
  for @{ 'xor_bool $a $b }.
 interpretation "xor_bool" 'xor_bool x y = (xor_bool x y).
 
+(* iteratore sugli esadecimali *)
+ndefinition forall_bool ≝ λP.P true ⊗ P false.
+
 ndefinition boolRelation : Type → Type ≝
 λA:Type.A → A → bool.