From 1a506c25fe9952e1fee371f164d11837619dbac7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 16 Nov 2008 10:30:30 +0000 Subject: [PATCH 1/1] fixed --- .../matita/library/didactic/exercises/duality.ma | 14 ++++++++++---- .../library/didactic/exercises/substitution.ma | 8 ++++++-- 2 files changed, 16 insertions(+), 6 deletions(-) diff --git a/helm/software/matita/library/didactic/exercises/duality.ma b/helm/software/matita/library/didactic/exercises/duality.ma index ea3a987d3..dca98ddc7 100644 --- a/helm/software/matita/library/didactic/exercises/duality.ma +++ b/helm/software/matita/library/didactic/exercises/duality.ma @@ -130,8 +130,10 @@ definition v20 ≝ λx. La semantica della formula `(A ∨ C)` nel mondo `v20` in cui `A` vale `2` e `C` vale `0` deve valere `1`. + Decommenta ed esegui. *) -eval normalize on [[FOr (FAtom 0) (FAtom 2)]]_v20. + +(* eval normalize on [[FOr (FAtom 0) (FAtom 2)]]_v20. *) (*DOCBEGIN @@ -188,10 +190,12 @@ let rec negate (F: Formula) on F : Formula ≝ Testare la funzione `negate`. Il risultato atteso è: - FOr (FNot (FAtom O)) (FImpl FTop (FNot (FAtom 1))) + FOr (FNot (FAtom O)) (FImpl FTop (FNot (FAtom 1))) + + Decommenta ed esegui *) -eval normalize on (negate (FOr (FAtom 0) (FImpl FTop (FAtom 1)))). +(* eval normalize on (negate (FOr (FAtom 0) (FImpl FTop (FAtom 1)))). *) (* ATTENZIONE ========== @@ -239,9 +243,11 @@ let rec dualize (F : Formula) on F : Formula ≝ Testare la funzione `dualize`. Il risultato atteso è: FAnd (FNot (FAtom O)) (FOr (FAtom 1) FTop) + + Decommenta ed esegui. *) -eval normalize on (dualize (FImpl (FAtom 0) (FAnd (FAtom 1) FBot))). +(* eval normalize on (dualize (FImpl (FAtom 0) (FAnd (FAtom 1) FBot))). *) (* Spiegazione =========== diff --git a/helm/software/matita/library/didactic/exercises/substitution.ma b/helm/software/matita/library/didactic/exercises/substitution.ma index 096b5b84c..0c9b86b00 100644 --- a/helm/software/matita/library/didactic/exercises/substitution.ma +++ b/helm/software/matita/library/didactic/exercises/substitution.ma @@ -232,7 +232,9 @@ definition v1101 ≝ λx. definition esempio1 ≝ (FImpl (FNot (FAtom 3)) (FOr (FAtom 2) (FAnd (FAtom 1) (FAtom 0)))). -eval normalize on [[ esempio1 ]]_v1101. +(* Decommenta ed esegui. *) + +(* eval normalize on [[ esempio1 ]]_v1101. *) (* Esercizio 3 @@ -303,7 +305,9 @@ definition esempio2 ≝ (FAnd (FImpl (FAtom 2) (FAtom 1)) (FAtom 2)). definition esempio3 ≝ (FOr (FAtom 0) (FAtom 1)). -eval normalize on (esempio2 [ esempio3 / 2]). +(* Decommenta ed esegui *) + +(* eval normalize on (esempio2 [ esempio3 / 2]). *) (*DOCBEGIN -- 2.39.2