helm/gTopLevel/tests/match02.cic.test

   1 [\lambda z:nat. \lambda h:(le 0 z). (le 0 (S z))]
   2 match (le_S 0 0 (le_n 0)): le with
   3 [ le_n \Rightarrow (le_S 0 0 (le_n 0))
   4 | (le_S x y) \Rightarrow (le_S 0 (S x) (le_S 0 x y)) ]
   5 ###### INTERPRETATION NUMBER 1 ######
   6 ### (* disambiguation environment  *)
   7 alias id S = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)
   8 alias id le = cic:/Coq/Init/Peano/le.ind#xpointer(1/1)
   9 alias id le_S = cic:/Coq/Init/Peano/le.ind#xpointer(1/1/2)
  10 alias id le_n = cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)
  11 alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
  12 alias num (instance 0) = "natural number"
  13 ### (* METASENV after disambiguation  *)
  14
  15 ### (* TERM after disambiguation      *)
  16
  17 <[z:nat][h:(le O z)](le O (S z))>Cases (le_S O O (le_n O)) of
  18  le_n => (le_S O O (le_n O))
  19  le_S => [x:nat][y:(le O x)](le_S O (S x) (le_S O x y))
  20 end
  21 ### (* TYPE_OF the disambiguated term *)
  22 ([z:nat][h:(le O z)](le O (S z)) (S O) (le_S O O (le_n O)))
  23 ### (* REDUCED disambiguated term     *)
  24 (le_S O (S O) (le_S O O (le_n O)))