From b763e29c46531b2bee8fabd35fa33746f0784d3b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 2 Oct 2008 11:20:43 +0000 Subject: [PATCH] ... --- helm/software/components/ng_kernel/TODO | 2 ++ 1 file changed, 2 insertions(+) diff --git a/helm/software/components/ng_kernel/TODO b/helm/software/components/ng_kernel/TODO index e37d7ffff..5e418e44b 100644 --- a/helm/software/components/ng_kernel/TODO +++ b/helm/software/components/ng_kernel/TODO @@ -10,6 +10,8 @@ e la si tagga con bound a seconda del test_eq_only <= k. ?1 <= Type_i -->> ?1 := ?2, ?2 : Type_i+1 +nel vecchio nucleo la height_of di un b-redex fa 0 e quindi riduci in forma normale + ------- ?1 = t (?1,?2)::(?2,t)::subst -- 2.39.2