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