85 \isatagquote |
85 \isatagquote |
86 % |
86 % |
87 \begin{isamarkuptext}% |
87 \begin{isamarkuptext}% |
88 \isaverbatim% |
88 \isaverbatim% |
89 \noindent% |
89 \noindent% |
90 \verb|dequeue :: forall a. Queue a -> (Maybe a, Queue a);|\newline% |
90 \hspace*{0pt}dequeue ::~forall a. Queue a -> (Maybe a, Queue a);\\ |
91 \verb|dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);|\newline% |
91 \hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y, Queue xs ys);\\ |
92 \verb|dequeue (Queue xs []) =|\newline% |
92 \hspace*{0pt}dequeue (Queue xs []) =\\ |
93 \verb| (if nulla xs then (Nothing, Queue [] [])|\newline% |
93 \hspace*{0pt} ~(if nulla xs then (Nothing, Queue [] [])\\ |
94 \verb| else dequeue (Queue [] (rev xs)));|% |
94 \hspace*{0pt} ~~~else dequeue (Queue [] (rev xs)));% |
95 \end{isamarkuptext}% |
95 \end{isamarkuptext}% |
96 \isamarkuptrue% |
96 \isamarkuptrue% |
97 % |
97 % |
98 \endisatagquote |
98 \endisatagquote |
99 {\isafoldquote}% |
99 {\isafoldquote}% |
271 \isatagquote |
271 \isatagquote |
272 % |
272 % |
273 \begin{isamarkuptext}% |
273 \begin{isamarkuptext}% |
274 \isaverbatim% |
274 \isaverbatim% |
275 \noindent% |
275 \noindent% |
276 \verb|module Example where {|\newline% |
276 \hspace*{0pt}module Example where {\char123}\\ |
277 \newline% |
277 \hspace*{0pt}\\ |
278 \newline% |
278 \hspace*{0pt}\\ |
279 \verb|data Nat = Suc Nat |\verb,|,\verb| Zero_nat;|\newline% |
279 \hspace*{0pt}data Nat = Suc Nat | Zero{\char95}nat;\\ |
280 \newline% |
280 \hspace*{0pt}\\ |
281 \verb|class Semigroup a where {|\newline% |
281 \hspace*{0pt}class Semigroup a where {\char123}\\ |
282 \verb| mult :: a -> a -> a;|\newline% |
282 \hspace*{0pt} ~mult ::~a -> a -> a;\\ |
283 \verb|};|\newline% |
283 \hspace*{0pt}{\char125};\\ |
284 \newline% |
284 \hspace*{0pt}\\ |
285 \verb|class (Semigroup a) => Monoid a where {|\newline% |
285 \hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\ |
286 \verb| neutral :: a;|\newline% |
286 \hspace*{0pt} ~neutral ::~a;\\ |
287 \verb|};|\newline% |
287 \hspace*{0pt}{\char125};\\ |
288 \newline% |
288 \hspace*{0pt}\\ |
289 \verb|pow :: forall a. (Monoid a) => Nat -> a -> a;|\newline% |
289 \hspace*{0pt}pow ::~forall a. (Monoid a) => Nat -> a -> a;\\ |
290 \verb|pow Zero_nat a = neutral;|\newline% |
290 \hspace*{0pt}pow Zero{\char95}nat a = neutral;\\ |
291 \verb|pow (Suc n) a = mult a (pow n a);|\newline% |
291 \hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\ |
292 \newline% |
292 \hspace*{0pt}\\ |
293 \verb|plus_nat :: Nat -> Nat -> Nat;|\newline% |
293 \hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\ |
294 \verb|plus_nat (Suc m) n = plus_nat m (Suc n);|\newline% |
294 \hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\ |
295 \verb|plus_nat Zero_nat n = n;|\newline% |
295 \hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\ |
296 \newline% |
296 \hspace*{0pt}\\ |
297 \verb|neutral_nat :: Nat;|\newline% |
297 \hspace*{0pt}neutral{\char95}nat ::~Nat;\\ |
298 \verb|neutral_nat = Suc Zero_nat;|\newline% |
298 \hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\ |
299 \newline% |
299 \hspace*{0pt}\\ |
300 \verb|mult_nat :: Nat -> Nat -> Nat;|\newline% |
300 \hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\ |
301 \verb|mult_nat Zero_nat n = Zero_nat;|\newline% |
301 \hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\ |
302 \verb|mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline% |
302 \hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ |
303 \newline% |
303 \hspace*{0pt}\\ |
304 \verb|instance Semigroup Nat where {|\newline% |
304 \hspace*{0pt}instance Semigroup Nat where {\char123}\\ |
305 \verb| mult = mult_nat;|\newline% |
305 \hspace*{0pt} ~mult = mult{\char95}nat;\\ |
306 \verb|};|\newline% |
306 \hspace*{0pt}{\char125};\\ |
307 \newline% |
307 \hspace*{0pt}\\ |
308 \verb|instance Monoid Nat where {|\newline% |
308 \hspace*{0pt}instance Monoid Nat where {\char123}\\ |
309 \verb| neutral = neutral_nat;|\newline% |
309 \hspace*{0pt} ~neutral = neutral{\char95}nat;\\ |
310 \verb|};|\newline% |
310 \hspace*{0pt}{\char125};\\ |
311 \newline% |
311 \hspace*{0pt}\\ |
312 \verb|bexp :: Nat -> Nat;|\newline% |
312 \hspace*{0pt}bexp ::~Nat -> Nat;\\ |
313 \verb|bexp n = pow n (Suc (Suc Zero_nat));|\newline% |
313 \hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\ |
314 \newline% |
314 \hspace*{0pt}\\ |
315 \verb|}|% |
315 \hspace*{0pt}{\char125}% |
316 \end{isamarkuptext}% |
316 \end{isamarkuptext}% |
317 \isamarkuptrue% |
317 \isamarkuptrue% |
318 % |
318 % |
319 \endisatagquote |
319 \endisatagquote |
320 {\isafoldquote}% |
320 {\isafoldquote}% |
336 \isatagquote |
336 \isatagquote |
337 % |
337 % |
338 \begin{isamarkuptext}% |
338 \begin{isamarkuptext}% |
339 \isaverbatim% |
339 \isaverbatim% |
340 \noindent% |
340 \noindent% |
341 \verb|structure Example = |\newline% |
341 \hspace*{0pt}structure Example = \\ |
342 \verb|struct|\newline% |
342 \hspace*{0pt}struct\\ |
343 \newline% |
343 \hspace*{0pt}\\ |
344 \verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline% |
344 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\ |
345 \newline% |
345 \hspace*{0pt}\\ |
346 \verb|type 'a semigroup = {mult : 'a -> 'a -> 'a};|\newline% |
346 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\ |
347 \verb|fun mult (A_:'a semigroup) = #mult A_;|\newline% |
347 \hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\ |
348 \newline% |
348 \hspace*{0pt}\\ |
349 \verb|type 'a monoid = {Program__semigroup_monoid : 'a semigroup, neutral : 'a};|\newline% |
349 \hspace*{0pt}type 'a monoid = {\char123}Program{\char95}{\char95}semigroup{\char95}monoid :~'a semigroup, neutral :~'a{\char125};\\ |
350 \verb|fun semigroup_monoid (A_:'a monoid) = #Program__semigroup_monoid A_;|\newline% |
350 \hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}Program{\char95}{\char95}semigroup{\char95}monoid A{\char95};\\ |
351 \verb|fun neutral (A_:'a monoid) = #neutral A_;|\newline% |
351 \hspace*{0pt}fun neutral (A{\char95}:'a monoid) = {\char35}neutral A{\char95};\\ |
352 \newline% |
352 \hspace*{0pt}\\ |
353 \verb|fun pow A_ Zero_nat a = neutral A_|\newline% |
353 \hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\ |
354 \verb| |\verb,|,\verb| pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a);|\newline% |
354 \hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\ |
355 \newline% |
355 \hspace*{0pt}\\ |
356 \verb|fun plus_nat (Suc m) n = plus_nat m (Suc n)|\newline% |
356 \hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\ |
357 \verb| |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline% |
357 \hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\ |
358 \newline% |
358 \hspace*{0pt}\\ |
359 \verb|val neutral_nat : nat = Suc Zero_nat;|\newline% |
359 \hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ |
360 \newline% |
360 \hspace*{0pt}\\ |
361 \verb|fun mult_nat Zero_nat n = Zero_nat|\newline% |
361 \hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\ |
362 \verb| |\verb,|,\verb| mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline% |
362 \hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ |
363 \newline% |
363 \hspace*{0pt}\\ |
364 \verb|val semigroup_nat = {mult = mult_nat} : nat semigroup;|\newline% |
364 \hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ |
365 \newline% |
365 \hspace*{0pt}\\ |
366 \verb|val monoid_nat =|\newline% |
366 \hspace*{0pt}val monoid{\char95}nat =\\ |
367 \verb| {Program__semigroup_monoid = semigroup_nat, neutral = neutral_nat} :|\newline% |
367 \hspace*{0pt} ~{\char123}Program{\char95}{\char95}semigroup{\char95}monoid = semigroup{\char95}nat, neutral = neutral{\char95}nat{\char125}~:\\ |
368 \verb| nat monoid;|\newline% |
368 \hspace*{0pt} ~nat monoid;\\ |
369 \newline% |
369 \hspace*{0pt}\\ |
370 \verb|fun bexp n = pow monoid_nat n (Suc (Suc Zero_nat));|\newline% |
370 \hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\ |
371 \newline% |
371 \hspace*{0pt}\\ |
372 \verb|end; (*struct Example*)|% |
372 \hspace*{0pt}end; (*struct Example*)% |
373 \end{isamarkuptext}% |
373 \end{isamarkuptext}% |
374 \isamarkuptrue% |
374 \isamarkuptrue% |
375 % |
375 % |
376 \endisatagquote |
376 \endisatagquote |
377 {\isafoldquote}% |
377 {\isafoldquote}% |
657 \isatagquote |
657 \isatagquote |
658 % |
658 % |
659 \begin{isamarkuptext}% |
659 \begin{isamarkuptext}% |
660 \isaverbatim% |
660 \isaverbatim% |
661 \noindent% |
661 \noindent% |
662 \verb|structure Example = |\newline% |
662 \hspace*{0pt}structure Example = \\ |
663 \verb|struct|\newline% |
663 \hspace*{0pt}struct\\ |
664 \newline% |
664 \hspace*{0pt}\\ |
665 \verb|datatype nat = Dig1 of nat |\verb,|,\verb| Dig0 of nat |\verb,|,\verb| One_nat |\verb,|,\verb| Zero_nat;|\newline% |
665 \hspace*{0pt}datatype nat = Dig1 of nat | Dig0 of nat | One{\char95}nat | Zero{\char95}nat;\\ |
666 \newline% |
666 \hspace*{0pt}\\ |
667 \verb|fun plus_nat (Dig1 m) (Dig1 n) = Dig0 (plus_nat (plus_nat m n) One_nat)|\newline% |
667 \hspace*{0pt}fun plus{\char95}nat (Dig1 m) (Dig1 n) = Dig0 (plus{\char95}nat (plus{\char95}nat m n) One{\char95}nat)\\ |
668 \verb| |\verb,|,\verb| plus_nat (Dig1 m) (Dig0 n) = Dig1 (plus_nat m n)|\newline% |
668 \hspace*{0pt} ~| plus{\char95}nat (Dig1 m) (Dig0 n) = Dig1 (plus{\char95}nat m n)\\ |
669 \verb| |\verb,|,\verb| plus_nat (Dig0 m) (Dig1 n) = Dig1 (plus_nat m n)|\newline% |
669 \hspace*{0pt} ~| plus{\char95}nat (Dig0 m) (Dig1 n) = Dig1 (plus{\char95}nat m n)\\ |
670 \verb| |\verb,|,\verb| plus_nat (Dig0 m) (Dig0 n) = Dig0 (plus_nat m n)|\newline% |
670 \hspace*{0pt} ~| plus{\char95}nat (Dig0 m) (Dig0 n) = Dig0 (plus{\char95}nat m n)\\ |
671 \verb| |\verb,|,\verb| plus_nat (Dig1 m) One_nat = Dig0 (plus_nat m One_nat)|\newline% |
671 \hspace*{0pt} ~| plus{\char95}nat (Dig1 m) One{\char95}nat = Dig0 (plus{\char95}nat m One{\char95}nat)\\ |
672 \verb| |\verb,|,\verb| plus_nat One_nat (Dig1 n) = Dig0 (plus_nat n One_nat)|\newline% |
672 \hspace*{0pt} ~| plus{\char95}nat One{\char95}nat (Dig1 n) = Dig0 (plus{\char95}nat n One{\char95}nat)\\ |
673 \verb| |\verb,|,\verb| plus_nat (Dig0 m) One_nat = Dig1 m|\newline% |
673 \hspace*{0pt} ~| plus{\char95}nat (Dig0 m) One{\char95}nat = Dig1 m\\ |
674 \verb| |\verb,|,\verb| plus_nat One_nat (Dig0 n) = Dig1 n|\newline% |
674 \hspace*{0pt} ~| plus{\char95}nat One{\char95}nat (Dig0 n) = Dig1 n\\ |
675 \verb| |\verb,|,\verb| plus_nat m Zero_nat = m|\newline% |
675 \hspace*{0pt} ~| plus{\char95}nat m Zero{\char95}nat = m\\ |
676 \verb| |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline% |
676 \hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\ |
677 \newline% |
677 \hspace*{0pt}\\ |
678 \verb|end; (*struct Example*)|% |
678 \hspace*{0pt}end; (*struct Example*)% |
679 \end{isamarkuptext}% |
679 \end{isamarkuptext}% |
680 \isamarkuptrue% |
680 \isamarkuptrue% |
681 % |
681 % |
682 \endisatagquote |
682 \endisatagquote |
683 {\isafoldquote}% |
683 {\isafoldquote}% |
774 \isatagquote |
774 \isatagquote |
775 % |
775 % |
776 \begin{isamarkuptext}% |
776 \begin{isamarkuptext}% |
777 \isaverbatim% |
777 \isaverbatim% |
778 \noindent% |
778 \noindent% |
779 \verb|structure Example = |\newline% |
779 \hspace*{0pt}structure Example = \\ |
780 \verb|struct|\newline% |
780 \hspace*{0pt}struct\\ |
781 \newline% |
781 \hspace*{0pt}\\ |
782 \verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline% |
782 \hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ |
783 \verb|fun eq (A_:'a eq) = #eq A_;|\newline% |
783 \hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\ |
784 \newline% |
784 \hspace*{0pt}\\ |
785 \verb|fun eqop A_ a b = eq A_ a b;|\newline% |
785 \hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\ |
786 \newline% |
786 \hspace*{0pt}\\ |
787 \verb|fun member A_ x [] = false|\newline% |
787 \hspace*{0pt}fun member A{\char95}~x [] = false\\ |
788 \verb| |\verb,|,\verb| member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys;|\newline% |
788 \hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqop A{\char95}~x y orelse member A{\char95}~x ys;\\ |
789 \newline% |
789 \hspace*{0pt}\\ |
790 \verb|fun collect_duplicates A_ xs ys [] = xs|\newline% |
790 \hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\ |
791 \verb| |\verb,|,\verb| collect_duplicates A_ xs ys (z :: zs) =|\newline% |
791 \hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\ |
792 \verb| (if member A_ z xs|\newline% |
792 \hspace*{0pt} ~~~(if member A{\char95}~z xs\\ |
793 \verb| then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline% |
793 \hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\ |
794 \verb| else collect_duplicates A_ xs (z :: ys) zs)|\newline% |
794 \hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\ |
795 \verb| else collect_duplicates A_ (z :: xs) (z :: ys) zs);|\newline% |
795 \hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\ |
796 \newline% |
796 \hspace*{0pt}\\ |
797 \verb|end; (*struct Example*)|% |
797 \hspace*{0pt}end; (*struct Example*)% |
798 \end{isamarkuptext}% |
798 \end{isamarkuptext}% |
799 \isamarkuptrue% |
799 \isamarkuptrue% |
800 % |
800 % |
801 \endisatagquote |
801 \endisatagquote |
802 {\isafoldquote}% |
802 {\isafoldquote}% |
910 \isatagquote |
910 \isatagquote |
911 % |
911 % |
912 \begin{isamarkuptext}% |
912 \begin{isamarkuptext}% |
913 \isaverbatim% |
913 \isaverbatim% |
914 \noindent% |
914 \noindent% |
915 \verb|structure Example = |\newline% |
915 \hspace*{0pt}structure Example = \\ |
916 \verb|struct|\newline% |
916 \hspace*{0pt}struct\\ |
917 \newline% |
917 \hspace*{0pt}\\ |
918 \verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline% |
918 \hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ |
919 \verb|fun eq (A_:'a eq) = #eq A_;|\newline% |
919 \hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\ |
920 \newline% |
920 \hspace*{0pt}\\ |
921 \verb|type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};|\newline% |
921 \hspace*{0pt}type 'a ord = {\char123}less{\char95}eq :~'a -> 'a -> bool, less :~'a -> 'a -> bool{\char125};\\ |
922 \verb|fun less_eq (A_:'a ord) = #less_eq A_;|\newline% |
922 \hspace*{0pt}fun less{\char95}eq (A{\char95}:'a ord) = {\char35}less{\char95}eq A{\char95};\\ |
923 \verb|fun less (A_:'a ord) = #less A_;|\newline% |
923 \hspace*{0pt}fun less (A{\char95}:'a ord) = {\char35}less A{\char95};\\ |
924 \newline% |
924 \hspace*{0pt}\\ |
925 \verb|fun eqop A_ a b = eq A_ a b;|\newline% |
925 \hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\ |
926 \newline% |
926 \hspace*{0pt}\\ |
927 \verb|type 'a preorder = {Orderings__ord_preorder : 'a ord};|\newline% |
927 \hspace*{0pt}type 'a preorder = {\char123}Orderings{\char95}{\char95}ord{\char95}preorder :~'a ord{\char125};\\ |
928 \verb|fun ord_preorder (A_:'a preorder) = #Orderings__ord_preorder A_;|\newline% |
928 \hspace*{0pt}fun ord{\char95}preorder (A{\char95}:'a preorder) = {\char35}Orderings{\char95}{\char95}ord{\char95}preorder A{\char95};\\ |
929 \newline% |
929 \hspace*{0pt}\\ |
930 \verb|type 'a order = {Orderings__preorder_order : 'a preorder};|\newline% |
930 \hspace*{0pt}type 'a order = {\char123}Orderings{\char95}{\char95}preorder{\char95}order :~'a preorder{\char125};\\ |
931 \verb|fun preorder_order (A_:'a order) = #Orderings__preorder_order A_;|\newline% |
931 \hspace*{0pt}fun preorder{\char95}order (A{\char95}:'a order) = {\char35}Orderings{\char95}{\char95}preorder{\char95}order A{\char95};\\ |
932 \newline% |
932 \hspace*{0pt}\\ |
933 \verb|fun less_eqa (A1_, A2_) B_ (x1, y1) (x2, y2) =|\newline% |
933 \hspace*{0pt}fun less{\char95}eqa (A1{\char95}, A2{\char95}) B{\char95}~(x1, y1) (x2, y2) =\\ |
934 \verb| less ((ord_preorder o preorder_order) A2_) x1 x2 orelse|\newline% |
934 \hspace*{0pt} ~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\ |
935 \verb| eqop A1_ x1 x2 andalso|\newline% |
935 \hspace*{0pt} ~~~eqop A1{\char95}~x1 x2 andalso\\ |
936 \verb| less_eq ((ord_preorder o preorder_order) B_) y1 y2|\newline% |
936 \hspace*{0pt} ~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2\\ |
937 \verb| |\verb,|,\verb| less_eqa (A1_, A2_) B_ (x1, y1) (x2, y2) =|\newline% |
937 \hspace*{0pt} ~| less{\char95}eqa (A1{\char95}, A2{\char95}) B{\char95}~(x1, y1) (x2, y2) =\\ |
938 \verb| less ((ord_preorder o preorder_order) A2_) x1 x2 orelse|\newline% |
938 \hspace*{0pt} ~~~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\ |
939 \verb| eqop A1_ x1 x2 andalso|\newline% |
939 \hspace*{0pt} ~~~~~eqop A1{\char95}~x1 x2 andalso\\ |
940 \verb| less_eq ((ord_preorder o preorder_order) B_) y1 y2;|\newline% |
940 \hspace*{0pt} ~~~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2;\\ |
941 \newline% |
941 \hspace*{0pt}\\ |
942 \verb|end; (*struct Example*)|% |
942 \hspace*{0pt}end; (*struct Example*)% |
943 \end{isamarkuptext}% |
943 \end{isamarkuptext}% |
944 \isamarkuptrue% |
944 \isamarkuptrue% |
945 % |
945 % |
946 \endisatagquote |
946 \endisatagquote |
947 {\isafoldquote}% |
947 {\isafoldquote}% |
1031 \isatagquote |
1031 \isatagquote |
1032 % |
1032 % |
1033 \begin{isamarkuptext}% |
1033 \begin{isamarkuptext}% |
1034 \isaverbatim% |
1034 \isaverbatim% |
1035 \noindent% |
1035 \noindent% |
1036 \verb|structure Example = |\newline% |
1036 \hspace*{0pt}structure Example = \\ |
1037 \verb|struct|\newline% |
1037 \hspace*{0pt}struct\\ |
1038 \newline% |
1038 \hspace*{0pt}\\ |
1039 \verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline% |
1039 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\ |
1040 \newline% |
1040 \hspace*{0pt}\\ |
1041 \verb|fun null [] = true|\newline% |
1041 \hspace*{0pt}fun null [] = true\\ |
1042 \verb| |\verb,|,\verb| null (x :: xs) = false;|\newline% |
1042 \hspace*{0pt} ~| null (x ::~xs) = false;\\ |
1043 \newline% |
1043 \hspace*{0pt}\\ |
1044 \verb|fun eq_nat (Suc a) Zero_nat = false|\newline% |
1044 \hspace*{0pt}fun eq{\char95}nat (Suc a) Zero{\char95}nat = false\\ |
1045 \verb| |\verb,|,\verb| eq_nat Zero_nat (Suc a) = false|\newline% |
1045 \hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc a) = false\\ |
1046 \verb| |\verb,|,\verb| eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'|\newline% |
1046 \hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\ |
1047 \verb| |\verb,|,\verb| eq_nat Zero_nat Zero_nat = true;|\newline% |
1047 \hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\ |
1048 \newline% |
1048 \hspace*{0pt}\\ |
1049 \verb|datatype monotype = Mono of nat * monotype list;|\newline% |
1049 \hspace*{0pt}datatype monotype = Mono of nat * monotype list;\\ |
1050 \newline% |
1050 \hspace*{0pt}\\ |
1051 \verb|fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys|\newline% |
1051 \hspace*{0pt}fun list{\char95}all2 p (x ::~xs) (y ::~ys) = p x y andalso list{\char95}all2 p xs ys\\ |
1052 \verb| |\verb,|,\verb| list_all2 p xs [] = null xs|\newline% |
1052 \hspace*{0pt} ~| list{\char95}all2 p xs [] = null xs\\ |
1053 \verb| |\verb,|,\verb| list_all2 p [] ys = null ys;|\newline% |
1053 \hspace*{0pt} ~| list{\char95}all2 p [] ys = null ys;\\ |
1054 \newline% |
1054 \hspace*{0pt}\\ |
1055 \verb|fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =|\newline% |
1055 \hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =\\ |
1056 \verb| eq_nat tyco1 tyco2 andalso list_all2 eq_monotype typargs1 typargs2;|\newline% |
1056 \hspace*{0pt} ~eq{\char95}nat tyco1 tyco2 andalso list{\char95}all2 eq{\char95}monotype typargs1 typargs2;\\ |
1057 \newline% |
1057 \hspace*{0pt}\\ |
1058 \verb|end; (*struct Example*)|% |
1058 \hspace*{0pt}end; (*struct Example*)% |
1059 \end{isamarkuptext}% |
1059 \end{isamarkuptext}% |
1060 \isamarkuptrue% |
1060 \isamarkuptrue% |
1061 % |
1061 % |
1062 \endisatagquote |
1062 \endisatagquote |
1063 {\isafoldquote}% |
1063 {\isafoldquote}% |
1106 \isatagquote |
1106 \isatagquote |
1107 % |
1107 % |
1108 \begin{isamarkuptext}% |
1108 \begin{isamarkuptext}% |
1109 \isaverbatim% |
1109 \isaverbatim% |
1110 \noindent% |
1110 \noindent% |
1111 \verb|strict_dequeue :: forall a. Queue a -> (a, Queue a);|\newline% |
1111 \hspace*{0pt}strict{\char95}dequeue ::~forall a. Queue a -> (a, Queue a);\\ |
1112 \verb|strict_dequeue (Queue xs (y : ys)) = (y, Queue xs ys);|\newline% |
1112 \hspace*{0pt}strict{\char95}dequeue (Queue xs (y :~ys)) = (y, Queue xs ys);\\ |
1113 \verb|strict_dequeue (Queue xs []) =|\newline% |
1113 \hspace*{0pt}strict{\char95}dequeue (Queue xs []) =\\ |
1114 \verb| let {|\newline% |
1114 \hspace*{0pt} ~let {\char123}\\ |
1115 \verb| (y : ys) = rev xs;|\newline% |
1115 \hspace*{0pt} ~~~(y :~ys) = rev xs;\\ |
1116 \verb| } in (y, Queue [] ys);|% |
1116 \hspace*{0pt} ~{\char125}~in (y, Queue [] ys);% |
1117 \end{isamarkuptext}% |
1117 \end{isamarkuptext}% |
1118 \isamarkuptrue% |
1118 \isamarkuptrue% |
1119 % |
1119 % |
1120 \endisatagquote |
1120 \endisatagquote |
1121 {\isafoldquote}% |
1121 {\isafoldquote}% |
1202 \isatagquote |
1202 \isatagquote |
1203 % |
1203 % |
1204 \begin{isamarkuptext}% |
1204 \begin{isamarkuptext}% |
1205 \isaverbatim% |
1205 \isaverbatim% |
1206 \noindent% |
1206 \noindent% |
1207 \verb|empty_queue :: forall a. a;|\newline% |
1207 \hspace*{0pt}empty{\char95}queue ::~forall a. a;\\ |
1208 \verb|empty_queue = error "empty_queue";|\newline% |
1208 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\ |
1209 \newline% |
1209 \hspace*{0pt}\\ |
1210 \verb|strict_dequeue' :: forall a. Queue a -> (a, Queue a);|\newline% |
1210 \hspace*{0pt}strict{\char95}dequeue' ::~forall a. Queue a -> (a, Queue a);\\ |
1211 \verb|strict_dequeue' (Queue xs []) =|\newline% |
1211 \hspace*{0pt}strict{\char95}dequeue' (Queue xs []) =\\ |
1212 \verb| (if nulla xs then empty_queue else strict_dequeue' (Queue [] (rev xs)));|\newline% |
1212 \hspace*{0pt} ~(if nulla xs then empty{\char95}queue else strict{\char95}dequeue' (Queue [] (rev xs)));\\ |
1213 \verb|strict_dequeue' (Queue xs (y : ys)) = (y, Queue xs ys);|% |
1213 \hspace*{0pt}strict{\char95}dequeue' (Queue xs (y :~ys)) = (y, Queue xs ys);% |
1214 \end{isamarkuptext}% |
1214 \end{isamarkuptext}% |
1215 \isamarkuptrue% |
1215 \isamarkuptrue% |
1216 % |
1216 % |
1217 \endisatagquote |
1217 \endisatagquote |
1218 {\isafoldquote}% |
1218 {\isafoldquote}% |