]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/tests/match01.cic.test
ignores .toc
[helm.git] / helm / gTopLevel / tests / match01.cic.test
1 [\lambda z:nat. \lambda h:(le O z). (eq nat O O)]
2 match (le_n O): le with
3 [ le_n \Rightarrow (refl_equal nat O)
4 | (le_S x y) \Rightarrow (refl_equal nat O) ]
5 ###### INTERPRETATION NUMBER 1 ######
6 ### (* disambiguation environment  *)
7 alias id O = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)
8 alias id eq = cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)
9 alias id le = cic:/Coq/Init/Peano/le.ind#xpointer(1/1)
10 alias id le_n = cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)
11 alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
12 alias id refl_equal = cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)
13 ### (* METASENV after disambiguation  *)
14
15 ### (* TERM after disambiguation      *)
16
17 <[z:nat][h:(le O z)](eq nat O O)>Cases (le_n O) of 
18  le_n => (refl_equal nat O)
19  le_S => [x:nat][y:(le O x)](refl_equal nat O)
20 end
21 ### (* TYPE_OF the disambiguated term *)
22 ([z:nat][h:(le O z)](eq nat O O) O (le_n O))
23 ### (* REDUCED disambiguated term     *)
24 (refl_equal nat O)