helm/gTopLevel/tests/match01.cic.test

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