]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/tests/lambda02.cic.test
2d813315c3aae8c6a5fd38671239b18d04c3d119
[helm.git] / helm / gTopLevel / tests / lambda02.cic.test
1 \lambda f:(\forall n:nat. (\forall H:(le 0 n). (n=n))). (f 0 (le_n 0))
2 ###### INTERPRETATION NUMBER 1 ######
3 ### (* disambiguation environment  *)
4 alias id le = cic:/Coq/Init/Peano/le.ind#xpointer(1/1)
5 alias id le_n = cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)
6 alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
7 alias num (instance 0) = "natural number"
8 alias symbol "eq" (instance 0) = "leibnitz's equality"
9 ### (* METASENV after disambiguation  *)
10
11 ### (* TERM after disambiguation      *)
12 [f:(n:nat)((le O n)->(eq nat n n))](f O (le_n O))
13 ### (* TYPE_OF the disambiguated term *)
14 (f:(n:nat)((le O n)->(eq nat n n)))(eq nat O O)
15 ### (* REDUCED disambiguated term     *)
16 [f:(n:nat)((le O n)->(eq nat n n))](f O (le_n O))