X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftests%2Flambda01.cic.test;h=6140de0b172be943097ccc687a20f1dbb6d5a1df;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=f05fb40db9fc85c2aba72ce1444a6d7f8767bcb9;hpb=aef0ab661736f065a2a41a09df6e79fd4e626cd7;p=helm.git diff --git a/helm/gTopLevel/tests/lambda01.cic.test b/helm/gTopLevel/tests/lambda01.cic.test index f05fb40db..6140de0b1 100644 --- a/helm/gTopLevel/tests/lambda01.cic.test +++ b/helm/gTopLevel/tests/lambda01.cic.test @@ -1,5 +1,11 @@ (\lambda f. (f 0 (le_n 0)) - \lambda n. \lambda H. (refl_equal nat 0))) + \lambda n. \lambda H. (refl_equal nat 0)) +###### INTERPRETATION NUMBER 1 ###### +### (* disambiguation environment *) +alias id le_n = cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1) +alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) +alias id refl_equal = cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1) +alias num (instance 0) = "natural number" ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *)