]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/tests/match06.cic.test
sort_of_prod relaxed to accept also Metas (when the second Meta has an
[helm.git] / helm / gTopLevel / tests / match06.cic.test
1 \lambda x:False.
2   [\lambda h:False. True]
3   match x:False with []
4 ### (* METASENV after disambiguation  *)
5
6 ### (* TERM after disambiguation      *)
7 [x:False]
8 <[h:False]True>Cases x of 
9 end
10 ### (* TYPE_OF the disambiguated term *)
11 (x:False)([h:False]True x)
12 ### (* REDUCED disambiguated term     *)
13 [x:False]
14 <[h:False]True>Cases x of 
15 end