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