From 8a62bb1bc12b3a40f54f9d77da204533fc215b0d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it> Date: Sat, 7 Feb 2004 17:58:39 +0000 Subject: [PATCH] A better (but yet not empty) metasenv is now returned. --- helm/gTopLevel/tests/lambda03.cic.test | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/helm/gTopLevel/tests/lambda03.cic.test b/helm/gTopLevel/tests/lambda03.cic.test index 0234af492..558be3839 100644 --- a/helm/gTopLevel/tests/lambda03.cic.test +++ b/helm/gTopLevel/tests/lambda03.cic.test @@ -1,12 +1,8 @@ \lambda n:nat. \lambda H:n=n.\lambda g:(?\to (le n 0))\to True.(g \lambda f.(f n H)) ### (* METASENV after disambiguation *) -n : nat; H : (eq nat n n); _ :? _; _ :? _; x : nat |- ?26: Type -n : nat; H : (eq nat n n); _ :? _; _ :? _; x : nat |- ?27: ?26[n ; H ; _ ; _ ; x] -n : nat; H : (eq nat n n); _ :? _ |- ?8: Type -n : nat; H : (eq nat n n); _ :? _ |- ?9: ?8[n ; H ; _] -n : nat; H : (eq nat n n) |- ?5: Type -n : nat; H : (eq nat n n) |- ?6: ?5[n ; H] + |- ?4: Type +n : nat; H : (eq nat n n) |- ?5: ?4[] ### (* TERM after disambiguation *) [n:nat][H:(eq nat n n)][g:(((x:nat)((eq nat x x)->(le x O))->(le n O))->True)](g [f:(x:nat)((eq nat x x)->(le x O))](f n H)) ### (* TYPE_OF the disambiguated term *) -- 2.39.5