Porting to intermediate syntax.

diff --git a/matita/matita/nlibrary/Plogic/equality.ma b/matita/matita/nlibrary/Plogic/equality.ma
index a5972e2709446cce6a401ba28c228e93920b54ac..eff29e26f3477b6712d93686623123ded01b4a9c 100644 (file)
--- a/matita/matita/nlibrary/Plogic/equality.ma
+++ b/matita/matita/nlibrary/Plogic/equality.ma
@@ -14,26 +14,26 @@
 
 include "logic/pts.ma".
 
-ninductive eq (A:Type[2]) (x:A) : A → Prop ≝
+inductive eq (A:Type[2]) (x:A) : A → Prop ≝
     refl: eq A x x.
     
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
-nlemma eq_rect_r:
- ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type. P a (refl A a) → P x p.
- #A; #a; #x; #p; ncases p; #P; #H; nassumption.
-nqed.
+lemma eq_rect_r:
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
+ #A; #a; #x; #p; cases p; #P; #H; assumption.
+qed.
 
-nlemma eq_ind_r :
+lemma eq_ind_r :
  ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ? ? ? p0); nassumption.
-nqed.
+ #A; #a; #P; #p; #x0; #p0; apply (eq_rect_r ? ? ? p0); assumption.
+qed.
 
-nlemma eq_rect_Type2_r :
-  ∀A:Type.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
-  #A;#a;#P;#H;#x;#p;ngeneralize in match H;ngeneralize in match P;
-  ncases p;//;
-nqed.
+lemma eq_rect_Type2_r :
+  ∀A:Type[0].∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+  #A;#a;#P;#H;#x;#p;generalize in match H;generalize in match P;
+  cases p;//;
+qed.
 
 (*
 nlemma eq_ind_r :

diff --git a/matita/matita/nlibrary/algebra/bool.ma b/matita/matita/nlibrary/algebra/bool.ma
index c3a7c6781a1317b479dd0cb2a387d063c67aca2a..a32f6c945fc0e3a270ee79e29629f724be8a42be 100644 (file)
--- a/matita/matita/nlibrary/algebra/bool.ma
+++ b/matita/matita/nlibrary/algebra/bool.ma
@@ -14,20 +14,20 @@
 
 include "logic/connectives.ma".
 
-ninductive eq (A: Type[1]) (a: A) : A → CProp[0] ≝
+inductive eq (A: Type[1]) (a: A) : A → CProp[0] ≝
  refl: eq A a a. 
 
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
  
-nlemma eq_ind_CProp0 : ∀A:Type[1].∀a:A.∀P:A → CProp[0].P a → ∀b:A.a = b → P b.
-#A; #a; #P; #p; #b; #E; ncases E; nassumption;
-nqed.
+lemma eq_ind_CProp0 : ∀A:Type[1].∀a:A.∀P:A → CProp[0].P a → ∀b:A.a = b → P b.
+#A; #a; #P; #p; #b; #E; cases E; assumption;
+qed.
 
-nlemma eq_ind_r_CProp0 : ∀A:Type[1].∀a:A.∀P:A → CProp[0].P a → ∀b:A.b = a → P b.
-#A; #a; #P; #p; #b; #E; ncases E in p; //;
-nqed. 
+lemma eq_ind_r_CProp0 : ∀A:Type[1].∀a:A.∀P:A → CProp[0].P a → ∀b:A.b = a → P b.
+#A; #a; #P; #p; #b; #E; cases E in p; //;
+qed. 
 
-nlemma csc : 
+lemma csc : 
  (∀x,y,z.(x∨(y∨z)) = ((x∨y)∨z)) →
  (∀x,y,z.(x∧(y∧z)) = ((x∧y)∧z)) →
  (∀x,y.(x∨y) = (y∨x)) →
@@ -47,7 +47,7 @@ nlemma csc :
  ∀a,b.((a ∧ ¬b) ∨ b) = (a ∨ b).
 #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8; #H9; #H10; #H11; #H12;
 #H13; #H14; #H15; #H16; #a; #b;
-nletin proof ≝ (
+letin proof ≝ (
 let clause_11: ∀x24. eq CProp[0] (And x24 True) x24
  ≝ λx24. H7 x24 in
  let clause_2: ∀x2. eq CProp[0] (Or x2 (Not x2)) True
@@ -86,5 +86,5 @@ let clause_11: ∀x24. eq CProp[0] (And x24 True) x24
                 (λx:CProp[0]. eq CProp[0] x (Or a b)) clause_190
                 (Or (And a (Not b)) b) (clause_15 (And a (Not b)) b) in
           clause_1);
-napply proof;
-nqed.
+apply proof;
+qed.

diff --git a/matita/matita/nlibrary/datatypes/bool.ma b/matita/matita/nlibrary/datatypes/bool.ma
index eda979d69b3c1121e76dadec86b5c789f8559086..044296559e674b0d1dce25b88b8e540fbaac74dc 100644 (file)
--- a/matita/matita/nlibrary/datatypes/bool.ma
+++ b/matita/matita/nlibrary/datatypes/bool.ma
@@ -14,9 +14,9 @@
 
 include "logic/pts.ma".
 
-ninductive bool: Type[0] ≝ true: bool | false: bool.
+inductive bool: Type[0] ≝ true: bool | false: bool.
  
-ndefinition orb ≝ λa,b:bool. match a with [ true ⇒ true | _ ⇒ b ].
+definition 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

diff --git a/matita/matita/nlibrary/hints_declaration.ma b/matita/matita/nlibrary/hints_declaration.ma
index 99aca7fa6e79fe01a6f086cded9bbc146b309a9a..88a5c7d7fcee867bd04914f76c7adf7f77cbaac5 100644 (file)
--- a/matita/matita/nlibrary/hints_declaration.ma
+++ b/matita/matita/nlibrary/hints_declaration.ma
@@ -58,12 +58,12 @@ notation > "≔ (list0 ( (list1 (ident x) sep , ) opt (: T) ) sep ,) opt (; (lis
 
 include "logic/pts.ma".
 
-ndefinition hint_declaration_Type0  ≝  λA:Type[0] .λa,b:A.Prop.
-ndefinition hint_declaration_Type1  ≝  λA:Type[1].λa,b:A.Prop.
-ndefinition hint_declaration_Type2  ≝  λa,b:Type[2].Prop.
-ndefinition hint_declaration_CProp0 ≝  λA:CProp[0].λa,b:A.Prop.
-ndefinition hint_declaration_CProp1 ≝  λA:CProp[1].λa,b:A.Prop.
-ndefinition hint_declaration_CProp2 ≝  λa,b:CProp[2].Prop.
+definition hint_declaration_Type0  ≝  λA:Type[0] .λa,b:A.Prop.
+definition hint_declaration_Type1  ≝  λA:Type[1].λa,b:A.Prop.
+definition hint_declaration_Type2  ≝  λa,b:Type[2].Prop.
+definition hint_declaration_CProp0 ≝  λA:CProp[0].λa,b:A.Prop.
+definition hint_declaration_CProp1 ≝  λA:CProp[1].λa,b:A.Prop.
+definition hint_declaration_CProp2 ≝  λa,b:CProp[2].Prop.
   
 interpretation "hint_decl_Type2"  'hint_decl a b = (hint_declaration_Type2 a b).
 interpretation "hint_decl_CProp2" 'hint_decl a b = (hint_declaration_CProp2 a b).
@@ -73,20 +73,20 @@ interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a
 interpretation "hint_decl_Type0"  'hint_decl a b = (hint_declaration_Type0 ? a b).
 
 (* Non uniform coercions support *)
-nrecord lock2 (S : Type[2]) (s : S) : Type[3] ≝ {
+record lock2 (S : Type[2]) (s : S) : Type[3] ≝ {
   force2 : Type[2];
   lift2  : force2
 }.
 
-nrecord lock1 (S : Type[1]) (s : S) : Type[2] ≝ {
+record lock1 (S : Type[1]) (s : S) : Type[2] ≝ {
   force1 : Type[1];
   lift1  : force1
 }.
 
-ncoercion lift1 : ∀S:Type[1].∀s:S.∀l:lock1 S s. force1 S s l ≝ lift1 
+coercion lift1 : ∀S:Type[1].∀s:S.∀l:lock1 S s. force1 S s l ≝ lift1 
  on s : ? to force1 ???.
 
-ncoercion lift2 : ∀S:Type[2].∀s:S.∀l:lock2 S s. force2 S s l ≝ lift2
+coercion lift2 : ∀S:Type[2].∀s:S.∀l:lock2 S s. force2 S s l ≝ lift2
  on s : ? to force2 ???.
 
 (* Example of a non uniform coercion declaration 
@@ -103,4 +103,4 @@ unification hint 0 ≔ R : setoid;
 (* ---------------------------------------- *) ⊢ 
    setoid ≡ force1 ? MR lock.
 
-*)
\ No newline at end of file
+*)