From: matitaweb Date: Mon, 7 Nov 2011 14:55:17 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2129 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1346bcc85bdce97c21f6dbcd503e8b17678e5f1b;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma index 228bffd51..80f49143a 100644 --- a/weblib/tutorial/chapter3.ma +++ b/weblib/tutorial/chapter3.ma @@ -114,7 +114,7 @@ match l with let rec nth n (A:Type[0]) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) (d:A) ≝ match n with - [O ⇒ a href="cic:/matita/tutorial/chapter3/hd.def(1)"hd/a A l d + [O ⇒ a href="cic:/matita/tutorial/chapter3/head.def(1)"head/a A l d |S m ⇒ nth m A (a href="cic:/matita/tutorial/chapter3/tail.def(1)"tail/a A l) d]. example ex_length: a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"length/a ? (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="nil" href="cic:/fakeuri.def(1)"[/a]) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a. @@ -258,7 +258,7 @@ A really convenient tool is the following combination of fold and filter, that essentially allow you to iterate on every subset of a given enumerated (finite) type, represented as a list. *) - let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (f:A→B) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l :B ≝ + let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"bool/a) (f:A→B) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l :B ≝ match l with [ nil ⇒ b | cons a l ⇒ a href="cic:/matita/basics/bool/if_then_else.def(1)"if_then_else/a ? (p a) (op (f a) (fold A B op b p f l))