helm/gTopLevel/tests/fix00.cic.test

   1 let rec fact =
   2   \lambda x:nat.
   3     [\lambda x:nat. nat]
   4     match x:nat with
   5     [ O \Rightarrow 1
   6     | (S (x: nat)) \Rightarrow (mult (S x) (fact x)) ]
   7 in
   8 (fact 4)
   9 ###### INTERPRETATION NUMBER 1 ######
  10 ### (* disambiguation environment  *)
  11 alias id S = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)
  12 alias id mult = cic:/Coq/Init/Peano/mult.con
  13 alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
  14 alias num (instance 0) = "natural number"
  15 ### (* METASENV after disambiguation  *)
  16
  17 ### (* TERM after disambiguation      *)
  18 [fact:=
  19 Fix fact {
  20 fact / 0 : (nat->nat) :=
  21 [x:nat]
  22 <[x:nat]nat>Cases x of
  23  O => (S O)
  24  S => [x:nat](mult (S x) (fact x))
  25 end}
  26 ](fact (S (S (S (S O)))))
  27 ### (* TYPE_OF the disambiguated term *)
  28 nat
  29 ### (* REDUCED disambiguated term     *)
  30 (S (
  31 Fix plus {
  32 plus / 0 : (nat->(nat->nat)) :=
  33 [n:nat][m:nat]
  34 <[n0:nat]nat>Cases n of
  35  O => m
  36  S => [p:nat](S (plus p m))
  37 end}
  38  (S (
  39 Fix plus {
  40 plus / 0 : (nat->(nat->nat)) :=
  41 [n:nat][m:nat]
  42 <[n0:nat]nat>Cases n of
  43  O => m
  44  S => [p:nat](S (plus p m))
  45 end}
  46  O (S (
  47 Fix plus {
  48 plus / 0 : (nat->(nat->nat)) :=
  49 [n:nat][m:nat]
  50 <[n0:nat]nat>Cases n of
  51  O => m
  52  S => [p:nat](S (plus p m))
  53 end}
  54  (S (
  55 Fix plus {
  56 plus / 0 : (nat->(nat->nat)) :=
  57 [n:nat][m:nat]
  58 <[n0:nat]nat>Cases n of
  59  O => m
  60  S => [p:nat](S (plus p m))
  61 end}
  62  O O)) (S (
  63 Fix plus {
  64 plus / 0 : (nat->(nat->nat)) :=
  65 [n:nat][m:nat]
  66 <[n0:nat]nat>Cases n of
  67  O => m
  68  S => [p:nat](S (plus p m))
  69 end}
  70  (S (
  71 Fix plus {
  72 plus / 0 : (nat->(nat->nat)) :=
  73 [n:nat][m:nat]
  74 <[n0:nat]nat>Cases n of
  75  O => m
  76  S => [p:nat](S (plus p m))
  77 end}
  78  O O)) O)))))) (S (
  79 Fix plus {
  80 plus / 0 : (nat->(nat->nat)) :=
  81 [n:nat][m:nat]
  82 <[n0:nat]nat>Cases n of
  83  O => m
  84  S => [p:nat](S (plus p m))
  85 end}
  86  (S (
  87 Fix plus {
  88 plus / 0 : (nat->(nat->nat)) :=
  89 [n:nat][m:nat]
  90 <[n0:nat]nat>Cases n of
  91  O => m
  92  S => [p:nat](S (plus p m))
  93 end}
  94  O (S (
  95 Fix plus {
  96 plus / 0 : (nat->(nat->nat)) :=
  97 [n:nat][m:nat]
  98 <[n0:nat]nat>Cases n of
  99  O => m
 100  S => [p:nat](S (plus p m))
 101 end}
 102  (S (
 103 Fix plus {
 104 plus / 0 : (nat->(nat->nat)) :=
 105 [n:nat][m:nat]
 106 <[n0:nat]nat>Cases n of
 107  O => m
 108  S => [p:nat](S (plus p m))
 109 end}
 110  O O)) (S (
 111 Fix plus {
 112 plus / 0 : (nat->(nat->nat)) :=
 113 [n:nat][m:nat]
 114 <[n0:nat]nat>Cases n of
 115  O => m
 116  S => [p:nat](S (plus p m))
 117 end}
 118  (S (
 119 Fix plus {
 120 plus / 0 : (nat->(nat->nat)) :=
 121 [n:nat][m:nat]
 122 <[n0:nat]nat>Cases n of
 123  O => m
 124  S => [p:nat](S (plus p m))
 125 end}
 126  O O)) O)))))) (S (
 127 Fix plus {
 128 plus / 0 : (nat->(nat->nat)) :=
 129 [n:nat][m:nat]
 130 <[n0:nat]nat>Cases n of
 131  O => m
 132  S => [p:nat](S (plus p m))
 133 end}
 134  (S (
 135 Fix plus {
 136 plus / 0 : (nat->(nat->nat)) :=
 137 [n:nat][m:nat]
 138 <[n0:nat]nat>Cases n of
 139  O => m
 140  S => [p:nat](S (plus p m))
 141 end}
 142  O (S (
 143 Fix plus {
 144 plus / 0 : (nat->(nat->nat)) :=
 145 [n:nat][m:nat]
 146 <[n0:nat]nat>Cases n of
 147  O => m
 148  S => [p:nat](S (plus p m))
 149 end}
 150  (S (
 151 Fix plus {
 152 plus / 0 : (nat->(nat->nat)) :=
 153 [n:nat][m:nat]
 154 <[n0:nat]nat>Cases n of
 155  O => m
 156  S => [p:nat](S (plus p m))
 157 end}
 158  O O)) (S (
 159 Fix plus {
 160 plus / 0 : (nat->(nat->nat)) :=
 161 [n:nat][m:nat]
 162 <[n0:nat]nat>Cases n of
 163  O => m
 164  S => [p:nat](S (plus p m))
 165 end}
 166  (S (
 167 Fix plus {
 168 plus / 0 : (nat->(nat->nat)) :=
 169 [n:nat][m:nat]
 170 <[n0:nat]nat>Cases n of
 171  O => m
 172  S => [p:nat](S (plus p m))
 173 end}
 174  O O)) O)))))) (S (
 175 Fix plus {
 176 plus / 0 : (nat->(nat->nat)) :=
 177 [n:nat][m:nat]
 178 <[n0:nat]nat>Cases n of
 179  O => m
 180  S => [p:nat](S (plus p m))
 181 end}
 182  (S (
 183 Fix plus {
 184 plus / 0 : (nat->(nat->nat)) :=
 185 [n:nat][m:nat]
 186 <[n0:nat]nat>Cases n of
 187  O => m
 188  S => [p:nat](S (plus p m))
 189 end}
 190  O (S (
 191 Fix plus {
 192 plus / 0 : (nat->(nat->nat)) :=
 193 [n:nat][m:nat]
 194 <[n0:nat]nat>Cases n of
 195  O => m
 196  S => [p:nat](S (plus p m))
 197 end}
 198  (S (
 199 Fix plus {
 200 plus / 0 : (nat->(nat->nat)) :=
 201 [n:nat][m:nat]
 202 <[n0:nat]nat>Cases n of
 203  O => m
 204  S => [p:nat](S (plus p m))
 205 end}
 206  O O)) (S (
 207 Fix plus {
 208 plus / 0 : (nat->(nat->nat)) :=
 209 [n:nat][m:nat]
 210 <[n0:nat]nat>Cases n of
 211  O => m
 212  S => [p:nat](S (plus p m))
 213 end}
 214  (S (
 215 Fix plus {
 216 plus / 0 : (nat->(nat->nat)) :=
 217 [n:nat][m:nat]
 218 <[n0:nat]nat>Cases n of
 219  O => m
 220  S => [p:nat](S (plus p m))
 221 end}
 222  O O)) O)))))) O))))))))