]> matita.cs.unibo.it Git - helm.git/commitdiff
Porting the new definition of equality.
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 18 Mar 2010 11:06:34 +0000 (11:06 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 18 Mar 2010 11:06:34 +0000 (11:06 +0000)
helm/software/matita/nlibrary/basics/bool.ma

index b8153d701ffd3d634402b8a8b24c71ff2724469a..5b93813f0f8377a9c97cb97b48645b99370912f2 100644 (file)
@@ -33,7 +33,8 @@ qed.*)
 
 (* ndestrcut does not work *)
 ntheorem not_eq_true_false : true \neq false.
-#Heq; nchange with match true with [true ⇒ False|false ⇒ True];
+napply nmk; #Heq;
+nchange with match true with [true ⇒ False|false ⇒ True];
 nrewrite > Heq; //; nqed.
 
 ndefinition notb : bool → bool ≝
@@ -107,10 +108,15 @@ ndefinition if_then_else: ∀A:Type. bool → A → A → A ≝
  [ true ⇒ P
  | false  ⇒ Q].
 
+(*
+ntheorem fff: false ≠ true.
+/2/;
+//; nqed. *)
+
 ntheorem bool_to_decidable_eq:
  ∀b1,b2:bool. decidable (b1=b2).
 #b1; #b2; ncases b1; ncases b2; /2/;
-@2;/2/; nqed.
+@2;/3/; nqed.
 
 ntheorem true_or_false:
 ∀b:bool. b = true ∨ b = false.