diff -r 1ca9055ba1f7 -r 985b13c5a61d doc-src/Codegen/Thy/document/Foundations.tex --- a/doc-src/Codegen/Thy/document/Foundations.tex Tue Sep 07 16:49:32 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Foundations.tex Tue Sep 07 16:58:01 2010 +0200 @@ -247,11 +247,11 @@ \begin{isamarkuptext}% \isatypewriter% \noindent% -\hspace*{0pt}dequeue ::~forall a.~Example.Queue a -> (Maybe a,~Example.Queue a);\\ -\hspace*{0pt}dequeue (Example.AQueue xs (y :~ys)) = (Just y,~Example.AQueue xs ys);\\ -\hspace*{0pt}dequeue (Example.AQueue xs []) =\\ -\hspace*{0pt} ~(if null xs then (Nothing,~Example.AQueue [] [])\\ -\hspace*{0pt} ~~~else Example.dequeue (Example.AQueue [] (reverse xs)));% +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ +\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ +\hspace*{0pt}dequeue (AQueue xs []) =\\ +\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\ +\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));% \end{isamarkuptext}% \isamarkuptrue% % @@ -444,12 +444,12 @@ \begin{isamarkuptext}% \isatypewriter% \noindent% -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Example.Queue a -> (a,~Example.Queue a);\\ -\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\ +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ \hspace*{0pt} ~let {\char123}\\ \hspace*{0pt} ~~~(y :~ys) = reverse xs;\\ -\hspace*{0pt} ~{\char125}~in (y,~Example.AQueue [] ys);\\ -\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.AQueue xs ys);% +\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\ +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);% \end{isamarkuptext}% \isamarkuptrue% % @@ -538,11 +538,11 @@ \hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\ \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\ \hspace*{0pt}\\ -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Example.Queue a -> (a,~Example.Queue a);\\ -\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.AQueue xs ys);\\ -\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\ -\hspace*{0pt} ~(if null xs then Example.empty{\char95}queue\\ -\hspace*{0pt} ~~~else Example.strict{\char95}dequeue (Example.AQueue [] (reverse xs)));% +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\ +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ +\hspace*{0pt} ~(if null xs then empty{\char95}queue\\ +\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));% \end{isamarkuptext}% \isamarkuptrue% %