From b660835a8e13fdbae35e0377b6f607e7db1c07a8 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Fri, 23 Mar 2012 08:51:09 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter1.ma | 2 +- weblib/tutorial/chapter8.ma | 2 -- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma index 7a961d4d2..9bb135c9a 100644 --- a/weblib/tutorial/chapter1.ma +++ b/weblib/tutorial/chapter1.ma @@ -206,7 +206,7 @@ cases b // qed. (* h2 class="section"Records/h2 It is time to proceed with our formalization of the farmer's problem. -A state of the system is defined by the position of four item: the goat, the +A state of the system is defined by the position of four items: the goat, the wolf, the cabbage, and the boat. The simplest way to declare such a data type is to use a record. *) diff --git a/weblib/tutorial/chapter8.ma b/weblib/tutorial/chapter8.ma index a84d10a2a..905e6604a 100644 --- a/weblib/tutorial/chapter8.ma +++ b/weblib/tutorial/chapter8.ma @@ -26,8 +26,6 @@ If we define then, we just have •(i1+i2) = •(i1)⊕ •(i2). *) -include "tutorial/chapter7.ma". - definition lo ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λa,b:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a a a title="pitem or" href="cic:/fakeuri.def(1)"+/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a b,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a a a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a b〉. notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}. interpretation "oplus" 'oplus a b = (lo ? a b). -- 2.39.2