X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftests%2Ffix00.cic.test;h=c3a4cfcd2380fafe4fa3f0cef929060398ac4433;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=901acd9904558f8fe78e3d7e03af94c5dca2b186;hpb=6ad08f90aa4a565d9b9dc54df32ddaf072506aad;p=helm.git

diff --git a/helm/gTopLevel/tests/fix00.cic.test b/helm/gTopLevel/tests/fix00.cic.test
index 901acd990..c3a4cfcd2 100644
--- a/helm/gTopLevel/tests/fix00.cic.test
+++ b/helm/gTopLevel/tests/fix00.cic.test
@@ -6,6 +6,12 @@ let rec fact =
     | (S (x: nat)) \Rightarrow (mult (S x) (fact x)) ]
 in
 (fact 4)
+###### INTERPRETATION NUMBER 1 ######
+### (* disambiguation environment  *)
+alias id S = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)
+alias id mult = cic:/Coq/Init/Peano/mult.con
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
+alias num (instance 0) = "natural number"
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)
@@ -23,7 +29,7 @@ nat
 ### (* REDUCED disambiguated term     *)
 (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -31,7 +37,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -39,7 +45,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -47,7 +53,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -55,7 +61,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -63,7 +69,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -71,7 +77,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O O)) O)))))) (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -79,7 +85,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -87,7 +93,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -95,7 +101,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -103,7 +109,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -111,7 +117,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -119,7 +125,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O O)) O)))))) (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -127,7 +133,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -135,7 +141,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -143,7 +149,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -151,7 +157,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -159,7 +165,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -167,7 +173,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O O)) O)))))) (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -175,7 +181,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -183,7 +189,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -191,7 +197,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -199,7 +205,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -207,7 +213,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m