TODO:
- "ncoercion" statement:
- - :> for projections
- simple syntax
- generation of hints to implement the pullback
- principles generation:
- - projections for records
- induction/inversions
- dependency graphs
- queries (on the trie?)
- ncut
- nclearbody
- nletin che prende il tipo
+ - napply che prenda il pattern
- Semantic selection:
- cosa usare per i pattern % ?
- compare with the paper
BUGS:
-
----- 1) nwhd non fa nulla ??? OK, testa rigida
+1) la disambiguazione sembra generare termini (? ? ?) quando buca!
+ inoltre buca anche quando c'e' una scelta sola
?2) cosa "corrisponde" alla simplify? multivm/breakpoint
=> la mu (+ iota) normalize
-3) nelim bacata (assert ...), ma napply funziona
- prod_lemmas/symmetric_eqquadruple, napply (Prod4T ...)
-*4) nrewrite bacata, ma napply funziona
*5) variabili libere => errore di tipaggio
6) sintassi per i NG naturali (serve una ndefault? serve una notazione
7) se c'' variabili locale x1 e il costruttore x1, fa due passate
8) exadecim_lemmas, destruct: lento...
-9) chiedere a Enrico il ninductive ascii_min che non va (ma cambiando il
- nome o il numero degli elementi invece si') ????
11) ngeneralize bug di unificazione: ngeneralize in match (x1 = x2)
12) generazione dei nomi non va:
include "freescale/byte8.ma".