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 ### (* METASENV after disambiguation  *)
   6
   7 ### (* TERM after disambiguation      *)
   8
   9 <[z:nat][h:(le O z)](eq nat O O)>Cases (le_n O) of
  10  le_n => (refl_equal nat O)
  11  le_S => [x:nat][y:(le O x)](refl_equal nat O)
  12 end
  13 ### (* TYPE_OF the disambiguated term *)
  14 ([z:nat][h:(le O z)](eq nat O O) O (le_n O))
  15 ### (* REDUCED disambiguated term     *)
  16 (refl_equal nat O)