From 5749216effe680d254a134a3a5230a8abaf69a88 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 17 Jul 2009 13:46:14 +0000 Subject: [PATCH] Some bugs already fixed. --- helm/software/matita/dist/TODO | 25 +++++++------------------ 1 file changed, 7 insertions(+), 18 deletions(-) diff --git a/helm/software/matita/dist/TODO b/helm/software/matita/dist/TODO index 628164c39..0fe3b959d 100644 --- a/helm/software/matita/dist/TODO +++ b/helm/software/matita/dist/TODO @@ -1,18 +1,19 @@ TODO: - "ncoercion" statement: - - type processing to identify source/target - - transitive closure (in the new Cic) + - :> for projections + - simple syntax - generation of hints to implement the pullback - principles generation: - - pretty printer for new statements required + - projections for records + - induction/inversions - dependency graphs - queries (on the trie?) -- serialization/undo - - objects - - ng_status (moo/lexicon) - Tactics: - satuation - destruct + - ncut + - nclearbody + - nletin che prende il tipo - Semantic selection: - cosa usare per i pattern % ? @@ -38,21 +39,9 @@ BUGS: 9) chiedere a Enrico il ninductive ascii_min che non va (ma cambiando il nome o il numero degli elementi invece si') ???? -10) enrivonment accetta nomi ripetuti 11) ngeneralize bug di unificazione: ngeneralize in match (x1 = x2) 12) generazione dei nomi non va: include "freescale/byte8.ma". nlemma test: ∀b1,b2,b3. plus_b8_d_d b1 (plus_b8_d_d b2 b3) = plus_b8_d_d (plus_b8_d_d b1 b2) b3. #b1; #b2; #b3; ncases b1; ncases b2; ncases b3; - -Tattiche mancanti: - - ncut - - nclearbody - - nletin che prende il tipo - -============= - -A) ng_tactics/nCicElim, ultime linee: commentare le prerr_endline -B) cut a mano (o quasi): - ncut (x1 = x2) lo implementi come nletin Hcut ≝ (? : x1 = x2) -- 2.39.2