From e01fb87a4768f2b2326cdc30f88cd239002ab511 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Feb 2004 14:27:38 +0000 Subject: [PATCH] ... --- helm/gTopLevel/tests/lambda01.cic.test | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/gTopLevel/tests/lambda01.cic.test b/helm/gTopLevel/tests/lambda01.cic.test index 0e1f8c22c..112856446 100644 --- a/helm/gTopLevel/tests/lambda01.cic.test +++ b/helm/gTopLevel/tests/lambda01.cic.test @@ -1,8 +1,8 @@ (\lambda f. (f 0 (le_n 0)) \lambda n. \lambda H. (refl_equal nat 0))) ### (* METASENV after disambiguation *) -f : (nat->((le O O)->(eq nat O O))); _ : nat |- ?14: Type -f : (nat->((le O O)->(eq nat O O))); _ : nat |- ?15: ?14[-2 ; -1] +_; _ : nat |- ?14: Type +_; _ : nat |- ?15: ?14[_ ; -1] ### (* TERM after disambiguation *) ([f:(nat->((le O O)->(eq nat O O)))](f O (le_n O)) [n:nat][H:(le O O)](refl_equal nat O)) ### (* TYPE_OF the disambiguated term *) -- 2.39.2