72 \isatagquote |
72 \isatagquote |
73 % |
73 % |
74 \begin{isamarkuptext}% |
74 \begin{isamarkuptext}% |
75 \isatypewriter% |
75 \isatypewriter% |
76 \noindent% |
76 \noindent% |
77 \hspace*{0pt}fib ::~Example.Nat -> Example.Nat;\\ |
77 \hspace*{0pt}fib ::~Nat -> Nat;\\ |
78 \hspace*{0pt}fib Example.Zero{\char95}nat = Example.Zero{\char95}nat;\\ |
78 \hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;\\ |
79 \hspace*{0pt}fib (Example.Suc Example.Zero{\char95}nat) = Example.Suc Example.Zero{\char95}nat;\\ |
79 \hspace*{0pt}fib (Suc Zero{\char95}nat) = Suc Zero{\char95}nat;\\ |
80 \hspace*{0pt}fib (Example.Suc (Example.Suc n)) =\\ |
80 \hspace*{0pt}fib (Suc (Suc n)) = plus{\char95}nat (fib n) (fib (Suc n));% |
81 \hspace*{0pt} ~Example.plus{\char95}nat (Example.fib n) (Example.fib (Example.Suc n));% |
|
82 \end{isamarkuptext}% |
81 \end{isamarkuptext}% |
83 \isamarkuptrue% |
82 \isamarkuptrue% |
84 % |
83 % |
85 \endisatagquote |
84 \endisatagquote |
86 {\isafoldquote}% |
85 {\isafoldquote}% |
171 \isatagquote |
170 \isatagquote |
172 % |
171 % |
173 \begin{isamarkuptext}% |
172 \begin{isamarkuptext}% |
174 \isatypewriter% |
173 \isatypewriter% |
175 \noindent% |
174 \noindent% |
176 \hspace*{0pt}fib{\char95}step ::~Example.Nat -> (Example.Nat,~Example.Nat);\\ |
175 \hspace*{0pt}fib{\char95}step ::~Nat -> (Nat,~Nat);\\ |
177 \hspace*{0pt}fib{\char95}step (Example.Suc n) =\\ |
176 \hspace*{0pt}fib{\char95}step (Suc n) = let {\char123}\\ |
178 \hspace*{0pt} ~let {\char123}\\ |
177 \hspace*{0pt} ~~~~~~~~~~~~~~~~~~~~(m,~q) = fib{\char95}step n;\\ |
179 \hspace*{0pt} ~~~(m,~q) = Example.fib{\char95}step n;\\ |
178 \hspace*{0pt} ~~~~~~~~~~~~~~~~~~{\char125}~in (plus{\char95}nat m q,~m);\\ |
180 \hspace*{0pt} ~{\char125}~in (Example.plus{\char95}nat m q,~m);\\ |
179 \hspace*{0pt}fib{\char95}step Zero{\char95}nat = (Suc Zero{\char95}nat,~Zero{\char95}nat);\\ |
181 \hspace*{0pt}fib{\char95}step Example.Zero{\char95}nat =\\ |
180 \hspace*{0pt}\\ |
182 \hspace*{0pt} ~(Example.Suc Example.Zero{\char95}nat,~Example.Zero{\char95}nat);\\ |
181 \hspace*{0pt}fib ::~Nat -> Nat;\\ |
183 \hspace*{0pt}\\ |
182 \hspace*{0pt}fib (Suc n) = fst (fib{\char95}step n);\\ |
184 \hspace*{0pt}fib ::~Example.Nat -> Example.Nat;\\ |
183 \hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;% |
185 \hspace*{0pt}fib (Example.Suc n) = fst (Example.fib{\char95}step n);\\ |
|
186 \hspace*{0pt}fib Example.Zero{\char95}nat = Example.Zero{\char95}nat;% |
|
187 \end{isamarkuptext}% |
184 \end{isamarkuptext}% |
188 \isamarkuptrue% |
185 \isamarkuptrue% |
189 % |
186 % |
190 \endisatagquote |
187 \endisatagquote |
191 {\isafoldquote}% |
188 {\isafoldquote}% |
591 \noindent% |
588 \noindent% |
592 \hspace*{0pt}module Example where {\char123}\\ |
589 \hspace*{0pt}module Example where {\char123}\\ |
593 \hspace*{0pt}\\ |
590 \hspace*{0pt}\\ |
594 \hspace*{0pt}newtype Dlist a = Dlist [a];\\ |
591 \hspace*{0pt}newtype Dlist a = Dlist [a];\\ |
595 \hspace*{0pt}\\ |
592 \hspace*{0pt}\\ |
596 \hspace*{0pt}empty ::~forall a.~Example.Dlist a;\\ |
593 \hspace*{0pt}empty ::~forall a.~Dlist a;\\ |
597 \hspace*{0pt}empty = Example.Dlist [];\\ |
594 \hspace*{0pt}empty = Dlist [];\\ |
598 \hspace*{0pt}\\ |
595 \hspace*{0pt}\\ |
599 \hspace*{0pt}member ::~forall a.~(Eq a) => [a] -> a -> Bool;\\ |
596 \hspace*{0pt}member ::~forall a.~(Eq a) => [a] -> a -> Bool;\\ |
600 \hspace*{0pt}member [] y = False;\\ |
597 \hspace*{0pt}member [] y = False;\\ |
601 \hspace*{0pt}member (x :~xs) y = x == y || Example.member xs y;\\ |
598 \hspace*{0pt}member (x :~xs) y = x == y || member xs y;\\ |
602 \hspace*{0pt}\\ |
599 \hspace*{0pt}\\ |
603 \hspace*{0pt}inserta ::~forall a.~(Eq a) => a -> [a] -> [a];\\ |
600 \hspace*{0pt}insert ::~forall a.~(Eq a) => a -> [a] -> [a];\\ |
604 \hspace*{0pt}inserta x xs = (if Example.member xs x then xs else x :~xs);\\ |
601 \hspace*{0pt}insert x xs = (if member xs x then xs else x :~xs);\\ |
605 \hspace*{0pt}\\ |
602 \hspace*{0pt}\\ |
606 \hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Example.Dlist a -> [a];\\ |
603 \hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Dlist a -> [a];\\ |
607 \hspace*{0pt}list{\char95}of{\char95}dlist (Example.Dlist x) = x;\\ |
604 \hspace*{0pt}list{\char95}of{\char95}dlist (Dlist x) = x;\\ |
608 \hspace*{0pt}\\ |
605 \hspace*{0pt}\\ |
609 \hspace*{0pt}insert ::~forall a.~(Eq a) => a -> Example.Dlist a -> Example.Dlist a;\\ |
606 \hspace*{0pt}inserta ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\ |
610 \hspace*{0pt}insert x dxs =\\ |
607 \hspace*{0pt}inserta x dxs = Dlist (insert x (list{\char95}of{\char95}dlist dxs));\\ |
611 \hspace*{0pt} ~Example.Dlist (Example.inserta x (Example.list{\char95}of{\char95}dlist dxs));\\ |
|
612 \hspace*{0pt}\\ |
608 \hspace*{0pt}\\ |
613 \hspace*{0pt}remove1 ::~forall a.~(Eq a) => a -> [a] -> [a];\\ |
609 \hspace*{0pt}remove1 ::~forall a.~(Eq a) => a -> [a] -> [a];\\ |
614 \hspace*{0pt}remove1 x [] = [];\\ |
610 \hspace*{0pt}remove1 x [] = [];\\ |
615 \hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~Example.remove1 x xs);\\ |
611 \hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~remove1 x xs);\\ |
616 \hspace*{0pt}\\ |
612 \hspace*{0pt}\\ |
617 \hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Example.Dlist a -> Example.Dlist a;\\ |
613 \hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\ |
618 \hspace*{0pt}remove x dxs =\\ |
614 \hspace*{0pt}remove x dxs = Dlist (remove1 x (list{\char95}of{\char95}dlist dxs));\\ |
619 \hspace*{0pt} ~Example.Dlist (Example.remove1 x (Example.list{\char95}of{\char95}dlist dxs));\\ |
|
620 \hspace*{0pt}\\ |
615 \hspace*{0pt}\\ |
621 \hspace*{0pt}{\char125}% |
616 \hspace*{0pt}{\char125}% |
622 \end{isamarkuptext}% |
617 \end{isamarkuptext}% |
623 \isamarkuptrue% |
618 \isamarkuptrue% |
624 % |
619 % |