From 1346bcc85bdce97c21f6dbcd503e8b17678e5f1b Mon Sep 17 00:00:00 2001 From: matitaweb Date: Mon, 7 Nov 2011 14:55:17 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter3.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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)) -- 2.39.2