From 07bbdce147ccdb1ca42bdfffc74f13a4dfae4d4d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 25 Sep 2008 16:10:27 +0000 Subject: [PATCH] ... --- helm/software/components/ng_kernel/TODO | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/helm/software/components/ng_kernel/TODO b/helm/software/components/ng_kernel/TODO index ed64039cb..e37d7ffff 100644 --- a/helm/software/components/ng_kernel/TODO +++ b/helm/software/components/ng_kernel/TODO @@ -3,7 +3,12 @@ in are_convertible togliere il caso Prop,Prop in quanto catturato da === in are_convertible togliere il caso Meta,Meta in quanto catturato da === in are_convertible caso Meta,Meta non fare lift ma accorcia il ctx +taggare le meta con tag::Type e in sort_of_prod verificare che i Pi +tra meta coinvolgano meta taggate. Il tag potrebbe contenere un bound, +in modo che si possano taggare anche meta quando si unifica ? ==vs== Type_k +e la si tagga con bound a seconda del test_eq_only <= k. +?1 <= Type_i -->> ?1 := ?2, ?2 : Type_i+1 ------- ?1 = t -- 2.39.2