]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/tests/fix00.cic.test
ocaml 3.09 transition
[helm.git] / helm / gTopLevel / tests / fix00.cic.test
index 8b3e333b82f46fe0863bbabd3b114dc6934a7b92..c3a4cfcd2380fafe4fa3f0cef929060398ac4433 100644 (file)
@@ -29,7 +29,7 @@ nat
 ### (* REDUCED disambiguated term     *)
 (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -37,7 +37,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -45,7 +45,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -53,7 +53,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -61,7 +61,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -69,7 +69,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -77,7 +77,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O O)) O)))))) (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -85,7 +85,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -93,7 +93,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -101,7 +101,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -109,7 +109,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -117,7 +117,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -125,7 +125,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O O)) O)))))) (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -133,7 +133,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -141,7 +141,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -149,7 +149,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -157,7 +157,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -165,7 +165,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -173,7 +173,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O O)) O)))))) (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -181,7 +181,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -189,7 +189,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -197,7 +197,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -205,7 +205,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -213,7 +213,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m