]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/tests/match06.cic.test
comments syntax changed
[helm.git] / helm / gTopLevel / tests / match06.cic.test
1 \lambda x:False.
2   [\lambda h:False. True]
3   match x:False with []
4 ###### INTERPRETATION NUMBER 1 ######
5 ### (* disambiguation environment  *)
6 alias id False = cic:/Coq/Init/Logic/False.ind#xpointer(1/1)
7 alias id True = cic:/Coq/Init/Logic/True.ind#xpointer(1/1)
8 ### (* METASENV after disambiguation  *)
9
10 ### (* TERM after disambiguation      *)
11 [x:False]
12 <[h:False]True>Cases x of 
13 end
14 ### (* TYPE_OF the disambiguated term *)
15 (x:False)([h:False]True x)
16 ### (* REDUCED disambiguated term     *)
17 [x:False]
18 <[h:False]True>Cases x of 
19 end