New chapter 4

[helm.git] / weblib / tutorial / chapter3.ma

diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma
index 45f834a8664703f3ea7a1296d2b8a27314b1441b..f7ad9155715878b850f9441dc9a1df70d4aaa716 100644 (file)
--- a/weblib/tutorial/chapter3.ma
+++ b/weblib/tutorial/chapter3.ma
@@ -262,7 +262,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→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"\ 6bool\ 5/a\ 6) (f:A→B) (l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝  
+ let rec fold (A,B:Type[0]) (op:B→B→B) (b:B) (p:A→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"\ 6bool\ 5/a\ 6) (f:A→B) (l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l:B ≝  
  match l with 
   [ nil ⇒ b 
   | cons a l ⇒ \ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? (p a) (op (f a) (fold A B op b p f l))