equal
deleted
inserted
replaced
83 \endisadelimquote |
83 \endisadelimquote |
84 % |
84 % |
85 \isatagquote |
85 \isatagquote |
86 % |
86 % |
87 \begin{isamarkuptext}% |
87 \begin{isamarkuptext}% |
88 \isaverbatim% |
88 \isatypewriter% |
89 \noindent% |
89 \noindent% |
90 \hspace*{0pt}dequeue ::~forall a. Queue a -> (Maybe a, Queue a);\\ |
90 \hspace*{0pt}dequeue ::~forall a. Queue a -> (Maybe a, Queue a);\\ |
91 \hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y, Queue xs ys);\\ |
91 \hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y, Queue xs ys);\\ |
92 \hspace*{0pt}dequeue (Queue xs []) =\\ |
92 \hspace*{0pt}dequeue (Queue xs []) =\\ |
93 \hspace*{0pt} ~(if nulla xs then (Nothing, Queue [] [])\\ |
93 \hspace*{0pt} ~(if nulla xs then (Nothing, Queue [] [])\\ |
269 \endisadelimquote |
269 \endisadelimquote |
270 % |
270 % |
271 \isatagquote |
271 \isatagquote |
272 % |
272 % |
273 \begin{isamarkuptext}% |
273 \begin{isamarkuptext}% |
274 \isaverbatim% |
274 \isatypewriter% |
275 \noindent% |
275 \noindent% |
276 \hspace*{0pt}module Example where {\char123}\\ |
276 \hspace*{0pt}module Example where {\char123}\\ |
277 \hspace*{0pt}\\ |
277 \hspace*{0pt}\\ |
278 \hspace*{0pt}\\ |
278 \hspace*{0pt}\\ |
279 \hspace*{0pt}data Nat = Suc Nat | Zero{\char95}nat;\\ |
279 \hspace*{0pt}data Nat = Suc Nat | Zero{\char95}nat;\\ |
334 \endisadelimquote |
334 \endisadelimquote |
335 % |
335 % |
336 \isatagquote |
336 \isatagquote |
337 % |
337 % |
338 \begin{isamarkuptext}% |
338 \begin{isamarkuptext}% |
339 \isaverbatim% |
339 \isatypewriter% |
340 \noindent% |
340 \noindent% |
341 \hspace*{0pt}structure Example = \\ |
341 \hspace*{0pt}structure Example = \\ |
342 \hspace*{0pt}struct\\ |
342 \hspace*{0pt}struct\\ |
343 \hspace*{0pt}\\ |
343 \hspace*{0pt}\\ |
344 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\ |
344 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\ |
655 \endisadelimquote |
655 \endisadelimquote |
656 % |
656 % |
657 \isatagquote |
657 \isatagquote |
658 % |
658 % |
659 \begin{isamarkuptext}% |
659 \begin{isamarkuptext}% |
660 \isaverbatim% |
660 \isatypewriter% |
661 \noindent% |
661 \noindent% |
662 \hspace*{0pt}structure Example = \\ |
662 \hspace*{0pt}structure Example = \\ |
663 \hspace*{0pt}struct\\ |
663 \hspace*{0pt}struct\\ |
664 \hspace*{0pt}\\ |
664 \hspace*{0pt}\\ |
665 \hspace*{0pt}datatype nat = Dig1 of nat | Dig0 of nat | One{\char95}nat | Zero{\char95}nat;\\ |
665 \hspace*{0pt}datatype nat = Dig1 of nat | Dig0 of nat | One{\char95}nat | Zero{\char95}nat;\\ |
772 \endisadelimquote |
772 \endisadelimquote |
773 % |
773 % |
774 \isatagquote |
774 \isatagquote |
775 % |
775 % |
776 \begin{isamarkuptext}% |
776 \begin{isamarkuptext}% |
777 \isaverbatim% |
777 \isatypewriter% |
778 \noindent% |
778 \noindent% |
779 \hspace*{0pt}structure Example = \\ |
779 \hspace*{0pt}structure Example = \\ |
780 \hspace*{0pt}struct\\ |
780 \hspace*{0pt}struct\\ |
781 \hspace*{0pt}\\ |
781 \hspace*{0pt}\\ |
782 \hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ |
782 \hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ |
908 \endisadelimquote |
908 \endisadelimquote |
909 % |
909 % |
910 \isatagquote |
910 \isatagquote |
911 % |
911 % |
912 \begin{isamarkuptext}% |
912 \begin{isamarkuptext}% |
913 \isaverbatim% |
913 \isatypewriter% |
914 \noindent% |
914 \noindent% |
915 \hspace*{0pt}structure Example = \\ |
915 \hspace*{0pt}structure Example = \\ |
916 \hspace*{0pt}struct\\ |
916 \hspace*{0pt}struct\\ |
917 \hspace*{0pt}\\ |
917 \hspace*{0pt}\\ |
918 \hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ |
918 \hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ |
1029 \endisadelimquote |
1029 \endisadelimquote |
1030 % |
1030 % |
1031 \isatagquote |
1031 \isatagquote |
1032 % |
1032 % |
1033 \begin{isamarkuptext}% |
1033 \begin{isamarkuptext}% |
1034 \isaverbatim% |
1034 \isatypewriter% |
1035 \noindent% |
1035 \noindent% |
1036 \hspace*{0pt}structure Example = \\ |
1036 \hspace*{0pt}structure Example = \\ |
1037 \hspace*{0pt}struct\\ |
1037 \hspace*{0pt}struct\\ |
1038 \hspace*{0pt}\\ |
1038 \hspace*{0pt}\\ |
1039 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\ |
1039 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\ |
1104 \endisadelimquote |
1104 \endisadelimquote |
1105 % |
1105 % |
1106 \isatagquote |
1106 \isatagquote |
1107 % |
1107 % |
1108 \begin{isamarkuptext}% |
1108 \begin{isamarkuptext}% |
1109 \isaverbatim% |
1109 \isatypewriter% |
1110 \noindent% |
1110 \noindent% |
1111 \hspace*{0pt}strict{\char95}dequeue ::~forall a. Queue a -> (a, Queue a);\\ |
1111 \hspace*{0pt}strict{\char95}dequeue ::~forall a. Queue a -> (a, Queue a);\\ |
1112 \hspace*{0pt}strict{\char95}dequeue (Queue xs (y :~ys)) = (y, Queue xs ys);\\ |
1112 \hspace*{0pt}strict{\char95}dequeue (Queue xs (y :~ys)) = (y, Queue xs ys);\\ |
1113 \hspace*{0pt}strict{\char95}dequeue (Queue xs []) =\\ |
1113 \hspace*{0pt}strict{\char95}dequeue (Queue xs []) =\\ |
1114 \hspace*{0pt} ~let {\char123}\\ |
1114 \hspace*{0pt} ~let {\char123}\\ |
1200 \endisadelimquote |
1200 \endisadelimquote |
1201 % |
1201 % |
1202 \isatagquote |
1202 \isatagquote |
1203 % |
1203 % |
1204 \begin{isamarkuptext}% |
1204 \begin{isamarkuptext}% |
1205 \isaverbatim% |
1205 \isatypewriter% |
1206 \noindent% |
1206 \noindent% |
1207 \hspace*{0pt}empty{\char95}queue ::~forall a. a;\\ |
1207 \hspace*{0pt}empty{\char95}queue ::~forall a. a;\\ |
1208 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\ |
1208 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\ |
1209 \hspace*{0pt}\\ |
1209 \hspace*{0pt}\\ |
1210 \hspace*{0pt}strict{\char95}dequeue' ::~forall a. Queue a -> (a, Queue a);\\ |
1210 \hspace*{0pt}strict{\char95}dequeue' ::~forall a. Queue a -> (a, Queue a);\\ |