helm/gTopLevel/tests/match00.cic.test

   1 [\lambda x:nat.
   2   [\lambda y:nat. Set]
   3     match x:nat with [ O \Rightarrow nat | (S x) \Rightarrow bool ]]
   4 match (S O):nat with
   5 [ O \Rightarrow O
   6 | (S x) \Rightarrow false ]
   7 ### (* METASENV after disambiguation  *)
   8
   9 ### (* TERM after disambiguation      *)
  10
  11 <[x:nat]
  12 <[y:nat]Set>Cases x of
  13  O => nat
  14  S => [x:nat]bool
  15 end>Cases (S O) of
  16  O => O
  17  S => [x:nat]false
  18 end
  19 ### (* TYPE_OF the disambiguated term *)
  20 ([x:nat]
  21 <[y:nat]Set>Cases x of
  22  O => nat
  23  S => [x:nat]bool
  24 end (S O))
  25 ### (* REDUCED disambiguated term     *)
  26 false