diff -r cfe74b0eecb1 -r 628fee3eb449 doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Tue Aug 17 14:19:12 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Tue Aug 17 14:19:12 2010 +0200 @@ -141,7 +141,8 @@ \isatypewriter% \noindent% \hspace*{0pt}structure Example :~sig\\ -\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\ +\hspace*{0pt} ~val id :~'a -> 'a\\ +\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\ \hspace*{0pt} ~val rev :~'a list -> 'a list\\ \hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\ \hspace*{0pt} ~val empty :~'a queue\\ @@ -149,10 +150,12 @@ \hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\ \hspace*{0pt}end = struct\\ \hspace*{0pt}\\ -\hspace*{0pt}fun foldl f a [] = a\\ -\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\ +\hspace*{0pt}fun id x = (fn xa => xa) x;\\ \hspace*{0pt}\\ -\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\ +\hspace*{0pt}fun fold f [] = id\\ +\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\ \hspace*{0pt}\\ \hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\ \hspace*{0pt}\\