]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_kernel/TODO
Use matita/lib as the new standard library in place of matita/nlibrary.
[helm.git] / matita / components / ng_kernel / TODO
1 muovere la split_prods nella riduzione e usarla nel caso di convertibilità di 2 match
2 in are_convertible togliere il caso Prop,Prop in quanto catturato da ===
3 in are_convertible togliere il caso Meta,Meta in quanto catturato da ===
4 in are_convertible caso Meta,Meta non fare lift ma accorcia il ctx
5
6 taggare le meta con tag::Type e in sort_of_prod verificare che i Pi
7 tra meta coinvolgano meta taggate. Il tag potrebbe contenere un bound,
8 in modo che si possano taggare anche meta quando si unifica ? ==vs== Type_k
9 e la si tagga con bound a seconda del test_eq_only <= k.
10
11 ?1 <= Type_i -->>  ?1 := ?2,   ?2 : Type_i+1
12
13 nel vecchio nucleo la height_of di un b-redex fa 0 e quindi riduci in forma
14 normale. Spostare la small_delta_step. 
15
16
17 @ tra universi senza duplicati
18 -------
19 ?1 = t
20   (?1,?2)::(?2,t)::subst
21   where ctx ?2 è minimale per t
22   poi le subst (?n,?m) le risolvi subito