helm/gTopLevel/tests/match05.cic.test

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