From 968c1c7745c0f5e4c06143c589fbec0cfc8f418c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 11 Jul 2005 14:05:32 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 914de2d4f..ebad4ed61 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -2,10 +2,6 @@ (**********************************************************************) TODO -- Bug: non disambigua - inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false). - perche' non inserisce nat nel domain di disambiguazione. Deve esserci un bug - stupido da qualche parte - preoccupante: per inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false). noi generiamo anche i_rec e i_rect che Coq non genera (e che NON dovrebbero @@ -68,10 +64,14 @@ TODO diversi/e DONE +- Bug: non disambigua + inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false). + perche' non inserisce nat nel domain di disambiguazione. Deve esserci un bug + stupido da qualche parte -> CSC - Bug vari nella generazione dei principi di eliminazione: 2. prodotti dipendenti come non-dipendenti (visibili eseguendo passo - passo il test inversion.ma) - 3. usato trucco outtype non dipendenti per il case + passo il test inversion.ma) -> CSC, Gares + 3. usato trucco outtype non dipendenti per il case -> CSC, Gares - controllo per script modificato o meno prima di uscire -> Gares - LApply deve prendere in input gli identificatori che va a generare; lascio a Ferruccio la scelta della sintassi concreta -> Ferruccio -- 2.39.2