From 766fd6c66d4317e6cd4b39a904905e05bdae51b6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 11 Jul 2005 14:17:37 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index ebad4ed61..81b104c3f 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -2,10 +2,10 @@ (**********************************************************************) TODO -- 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 - essere accettati dal nostro nucleo che invece non fa una piega!!!) +- PREOCCUPANTE: per + inductive i : Prop := K : True (*-> i*) -> i. + noi generiamo i_rec e i_rect con e senza il commento qui sopra; Coq NON + genera i_rec e i_rect quando c'e' un argomento ricorsivo - parsing contestuale (tattiche replace, change e forse altre) - assiomi - Guardare il commento -- 2.39.2