helm/gTopLevel/tests/match07.cic.test

   1 [\lambda x:bool. nat]
   2 match true with
   3 [ true \Rightarrow O
   4 | false \Rightarrow (S O) ]
   5 ### (* METASENV after disambiguation  *)
   6
   7 ### (* TERM after disambiguation      *)
   8
   9 <[x:bool]nat>Cases true of
  10  true => O
  11  false => (S O)
  12 end
  13 ### (* TYPE_OF the disambiguated term *)
  14 ([x:bool]nat true)
  15 ### (* REDUCED disambiguated term     *)
  16 O