]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/tests/forall00.cic.test
ignores .toc
[helm.git] / helm / gTopLevel / tests / forall00.cic.test
1 \forall n:nat. \forall m. n + m = n
2 ###### INTERPRETATION NUMBER 1 ######
3 ### (* disambiguation environment  *)
4 alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
5 alias symbol "eq" (instance 0) = "leibnitz's equality"
6 alias symbol "plus" (instance 0) = "natural plus"
7 ### (* METASENV after disambiguation  *)
8
9 ### (* TERM after disambiguation      *)
10 (n:nat)(m:nat)(eq nat (plus n m) n)
11 ### (* TYPE_OF the disambiguated term *)
12 Prop
13 ### (* REDUCED disambiguated term     *)
14 (n:nat)(m:nat)(eq nat (plus n m) n)