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

diff --git a/helm/gTopLevel/tests/fix00.cic.test b/helm/gTopLevel/tests/fix00.cic.test
index f688c4060..c3a4cfcd2 100644
--- a/helm/gTopLevel/tests/fix00.cic.test
+++ b/helm/gTopLevel/tests/fix00.cic.test
@@ -6,9 +6,14 @@ 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  *)
- |- ?2: Type
- |- ?3: ?2[]
+
 ### (* TERM after disambiguation      *)
 [fact:=
 Fix fact {
@@ -24,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
@@ -32,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
@@ -40,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
@@ -48,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
@@ -56,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
@@ -64,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
@@ -72,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
@@ -80,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
@@ -88,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
@@ -96,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
@@ -104,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
@@ -112,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
@@ -120,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
@@ -128,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
@@ -136,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
@@ -144,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
@@ -152,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
@@ -160,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
@@ -168,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
@@ -176,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
@@ -184,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
@@ -192,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
@@ -200,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
@@ -208,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