1.1 --- a/doc-src/Classes/Thy/document/Classes.tex	Tue Sep 07 16:49:32 2010 +0200
     1.2 +++ b/doc-src/Classes/Thy/document/Classes.tex	Tue Sep 07 16:58:01 2010 +0200
     1.3 @@ -1134,65 +1134,64 @@
     1.4  \noindent%
     1.5  \hspace*{0pt}module Example where {\char123}\\
     1.6  \hspace*{0pt}\\
     1.7 -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Example.Nat;\\
     1.8 +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
     1.9  \hspace*{0pt}\\
    1.10 -\hspace*{0pt}nat{\char95}aux ::~Integer -> Example.Nat -> Example.Nat;\\
    1.11 -\hspace*{0pt}nat{\char95}aux i n =\\
    1.12 -\hspace*{0pt} ~(if i <= 0 then n else Example.nat{\char95}aux (i - 1) (Example.Suc n));\\
    1.13 +\hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
    1.14 +\hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
    1.15  \hspace*{0pt}\\
    1.16 -\hspace*{0pt}nat ::~Integer -> Example.Nat;\\
    1.17 -\hspace*{0pt}nat i = Example.nat{\char95}aux i Example.Zero{\char95}nat;\\
    1.18 +\hspace*{0pt}nat ::~Integer -> Nat;\\
    1.19 +\hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\
    1.20  \hspace*{0pt}\\
    1.21  \hspace*{0pt}class Semigroup a where {\char123}\\
    1.22  \hspace*{0pt} ~mult ::~a -> a -> a;\\
    1.23  \hspace*{0pt}{\char125};\\
    1.24  \hspace*{0pt}\\
    1.25 -\hspace*{0pt}class (Example.Semigroup a) => Monoidl a where {\char123}\\
    1.26 +\hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\
    1.27  \hspace*{0pt} ~neutral ::~a;\\
    1.28  \hspace*{0pt}{\char125};\\
    1.29  \hspace*{0pt}\\
    1.30 -\hspace*{0pt}class (Example.Monoidl a) => Monoid a where {\char123}\\
    1.31 +\hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\
    1.32  \hspace*{0pt}{\char125};\\
    1.33  \hspace*{0pt}\\
    1.34 -\hspace*{0pt}class (Example.Monoid a) => Group a where {\char123}\\
    1.35 +\hspace*{0pt}class (Monoid a) => Group a where {\char123}\\
    1.36  \hspace*{0pt} ~inverse ::~a -> a;\\
    1.37  \hspace*{0pt}{\char125};\\
    1.38  \hspace*{0pt}\\
    1.39 +\hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
    1.40 +\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
    1.41 +\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
    1.42 +\hspace*{0pt}\\
    1.43 +\hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
    1.44 +\hspace*{0pt}pow{\char95}int k x =\\
    1.45 +\hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\
    1.46 +\hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\
    1.47 +\hspace*{0pt}\\
    1.48  \hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\
    1.49  \hspace*{0pt}mult{\char95}int i j = i + j;\\
    1.50  \hspace*{0pt}\\
    1.51 +\hspace*{0pt}instance Semigroup Integer where {\char123}\\
    1.52 +\hspace*{0pt} ~mult = mult{\char95}int;\\
    1.53 +\hspace*{0pt}{\char125};\\
    1.54 +\hspace*{0pt}\\
    1.55  \hspace*{0pt}neutral{\char95}int ::~Integer;\\
    1.56  \hspace*{0pt}neutral{\char95}int = 0;\\
    1.57  \hspace*{0pt}\\
    1.58 +\hspace*{0pt}instance Monoidl Integer where {\char123}\\
    1.59 +\hspace*{0pt} ~neutral = neutral{\char95}int;\\
    1.60 +\hspace*{0pt}{\char125};\\
    1.61 +\hspace*{0pt}\\
    1.62 +\hspace*{0pt}instance Monoid Integer where {\char123}\\
    1.63 +\hspace*{0pt}{\char125};\\
    1.64 +\hspace*{0pt}\\
    1.65  \hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\
    1.66  \hspace*{0pt}inverse{\char95}int i = negate i;\\
    1.67  \hspace*{0pt}\\
    1.68 -\hspace*{0pt}instance Example.Semigroup Integer where {\char123}\\
    1.69 -\hspace*{0pt} ~mult = Example.mult{\char95}int;\\
    1.70 +\hspace*{0pt}instance Group Integer where {\char123}\\
    1.71 +\hspace*{0pt} ~inverse = inverse{\char95}int;\\
    1.72  \hspace*{0pt}{\char125};\\
    1.73  \hspace*{0pt}\\
    1.74 -\hspace*{0pt}instance Example.Monoidl Integer where {\char123}\\
    1.75 -\hspace*{0pt} ~neutral = Example.neutral{\char95}int;\\
    1.76 -\hspace*{0pt}{\char125};\\
    1.77 -\hspace*{0pt}\\
    1.78 -\hspace*{0pt}instance Example.Monoid Integer where {\char123}\\
    1.79 -\hspace*{0pt}{\char125};\\
    1.80 -\hspace*{0pt}\\
    1.81 -\hspace*{0pt}instance Example.Group Integer where {\char123}\\
    1.82 -\hspace*{0pt} ~inverse = Example.inverse{\char95}int;\\
    1.83 -\hspace*{0pt}{\char125};\\
    1.84 -\hspace*{0pt}\\
    1.85 -\hspace*{0pt}pow{\char95}nat ::~forall a.~(Example.Monoid a) => Example.Nat -> a -> a;\\
    1.86 -\hspace*{0pt}pow{\char95}nat Example.Zero{\char95}nat x = Example.neutral;\\
    1.87 -\hspace*{0pt}pow{\char95}nat (Example.Suc n) x = Example.mult x (Example.pow{\char95}nat n x);\\
    1.88 -\hspace*{0pt}\\
    1.89 -\hspace*{0pt}pow{\char95}int ::~forall a.~(Example.Group a) => Integer -> a -> a;\\
    1.90 -\hspace*{0pt}pow{\char95}int k x =\\
    1.91 -\hspace*{0pt} ~(if 0 <= k then Example.pow{\char95}nat (Example.nat k) x\\
    1.92 -\hspace*{0pt} ~~~else Example.inverse (Example.pow{\char95}nat (Example.nat (negate k)) x));\\
    1.93 -\hspace*{0pt}\\
    1.94  \hspace*{0pt}example ::~Integer;\\
    1.95 -\hspace*{0pt}example = Example.pow{\char95}int 10 (-2);\\
    1.96 +\hspace*{0pt}example = pow{\char95}int 10 (-2);\\
    1.97  \hspace*{0pt}\\
    1.98  \hspace*{0pt}{\char125}%
    1.99  \end{isamarkuptext}%

     2.1 --- a/doc-src/Codegen/Thy/document/Foundations.tex	Tue Sep 07 16:49:32 2010 +0200
     2.2 +++ b/doc-src/Codegen/Thy/document/Foundations.tex	Tue Sep 07 16:58:01 2010 +0200
     2.3 @@ -247,11 +247,11 @@
     2.4  \begin{isamarkuptext}%
     2.5  \isatypewriter%
     2.6  \noindent%
     2.7 -\hspace*{0pt}dequeue ::~forall a.~Example.Queue a -> (Maybe a,~Example.Queue a);\\
     2.8 -\hspace*{0pt}dequeue (Example.AQueue xs (y :~ys)) = (Just y,~Example.AQueue xs ys);\\
     2.9 -\hspace*{0pt}dequeue (Example.AQueue xs []) =\\
    2.10 -\hspace*{0pt} ~(if null xs then (Nothing,~Example.AQueue [] [])\\
    2.11 -\hspace*{0pt} ~~~else Example.dequeue (Example.AQueue [] (reverse xs)));%
    2.12 +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
    2.13 +\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
    2.14 +\hspace*{0pt}dequeue (AQueue xs []) =\\
    2.15 +\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
    2.16 +\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
    2.17  \end{isamarkuptext}%
    2.18  \isamarkuptrue%
    2.19  %
    2.20 @@ -444,12 +444,12 @@
    2.21  \begin{isamarkuptext}%
    2.22  \isatypewriter%
    2.23  \noindent%
    2.24 -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Example.Queue a -> (a,~Example.Queue a);\\
    2.25 -\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\
    2.26 +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
    2.27 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
    2.28  \hspace*{0pt} ~let {\char123}\\
    2.29  \hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
    2.30 -\hspace*{0pt} ~{\char125}~in (y,~Example.AQueue [] ys);\\
    2.31 -\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.AQueue xs ys);%
    2.32 +\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
    2.33 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
    2.34  \end{isamarkuptext}%
    2.35  \isamarkuptrue%
    2.36  %
    2.37 @@ -538,11 +538,11 @@
    2.38  \hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
    2.39  \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
    2.40  \hspace*{0pt}\\
    2.41 -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Example.Queue a -> (a,~Example.Queue a);\\
    2.42 -\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.AQueue xs ys);\\
    2.43 -\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\
    2.44 -\hspace*{0pt} ~(if null xs then Example.empty{\char95}queue\\
    2.45 -\hspace*{0pt} ~~~else Example.strict{\char95}dequeue (Example.AQueue [] (reverse xs)));%
    2.46 +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
    2.47 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
    2.48 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
    2.49 +\hspace*{0pt} ~(if null xs then empty{\char95}queue\\
    2.50 +\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));%
    2.51  \end{isamarkuptext}%
    2.52  \isamarkuptrue%
    2.53  %

     3.1 --- a/doc-src/Codegen/Thy/document/Further.tex	Tue Sep 07 16:49:32 2010 +0200
     3.2 +++ b/doc-src/Codegen/Thy/document/Further.tex	Tue Sep 07 16:58:01 2010 +0200
     3.3 @@ -216,13 +216,13 @@
     3.4  \begin{isamarkuptext}%
     3.5  \isatypewriter%
     3.6  \noindent%
     3.7 -\hspace*{0pt}funpow ::~forall a.~Example.Nat -> (a -> a) -> a -> a;\\
     3.8 -\hspace*{0pt}funpow Example.Zero{\char95}nat f = id;\\
     3.9 -\hspace*{0pt}funpow (Example.Suc n) f = f .~Example.funpow n f;\\
    3.10 +\hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\
    3.11 +\hspace*{0pt}funpow Zero{\char95}nat f = id;\\
    3.12 +\hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\
    3.13  \hspace*{0pt}\\
    3.14 -\hspace*{0pt}funpows ::~forall a.~[Example.Nat] -> (a -> a) -> a -> a;\\
    3.15 +\hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\
    3.16  \hspace*{0pt}funpows [] = id;\\
    3.17 -\hspace*{0pt}funpows (x :~xs) = Example.funpow x .~Example.funpows xs;%
    3.18 +\hspace*{0pt}funpows (x :~xs) = funpow x .~funpows xs;%
    3.19  \end{isamarkuptext}%
    3.20  \isamarkuptrue%
    3.21  %

     4.1 --- a/doc-src/Codegen/Thy/document/Introduction.tex	Tue Sep 07 16:49:32 2010 +0200
     4.2 +++ b/doc-src/Codegen/Thy/document/Introduction.tex	Tue Sep 07 16:58:01 2010 +0200
     4.3 @@ -231,19 +231,19 @@
     4.4  \hspace*{0pt}\\
     4.5  \hspace*{0pt}data Queue a = AQueue [a] [a];\\
     4.6  \hspace*{0pt}\\
     4.7 -\hspace*{0pt}empty ::~forall a.~Example.Queue a;\\
     4.8 -\hspace*{0pt}empty = Example.AQueue [] [];\\
     4.9 +\hspace*{0pt}empty ::~forall a.~Queue a;\\
    4.10 +\hspace*{0pt}empty = AQueue [] [];\\
    4.11  \hspace*{0pt}\\
    4.12 -\hspace*{0pt}dequeue ::~forall a.~Example.Queue a -> (Maybe a,~Example.Queue a);\\
    4.13 -\hspace*{0pt}dequeue (Example.AQueue [] []) = (Nothing,~Example.AQueue [] []);\\
    4.14 -\hspace*{0pt}dequeue (Example.AQueue xs (y :~ys)) = (Just y,~Example.AQueue xs ys);\\
    4.15 -\hspace*{0pt}dequeue (Example.AQueue (v :~va) []) =\\
    4.16 +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
    4.17 +\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\
    4.18 +\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
    4.19 +\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\
    4.20  \hspace*{0pt} ~let {\char123}\\
    4.21  \hspace*{0pt} ~~~(y :~ys) = reverse (v :~va);\\
    4.22 -\hspace*{0pt} ~{\char125}~in (Just y,~Example.AQueue [] ys);\\
    4.23 +\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
    4.24  \hspace*{0pt}\\
    4.25 -\hspace*{0pt}enqueue ::~forall a.~a -> Example.Queue a -> Example.Queue a;\\
    4.26 -\hspace*{0pt}enqueue x (Example.AQueue xs ys) = Example.AQueue (x :~xs) ys;\\
    4.27 +\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
    4.28 +\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
    4.29  \hspace*{0pt}\\
    4.30  \hspace*{0pt}{\char125}%
    4.31  \end{isamarkuptext}%
    4.32 @@ -397,41 +397,41 @@
    4.33  \noindent%
    4.34  \hspace*{0pt}module Example where {\char123}\\
    4.35  \hspace*{0pt}\\
    4.36 -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Example.Nat;\\
    4.37 +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
    4.38  \hspace*{0pt}\\
    4.39 -\hspace*{0pt}plus{\char95}nat ::~Example.Nat -> Example.Nat -> Example.Nat;\\
    4.40 -\hspace*{0pt}plus{\char95}nat (Example.Suc m) n = Example.plus{\char95}nat m (Example.Suc n);\\
    4.41 -\hspace*{0pt}plus{\char95}nat Example.Zero{\char95}nat n = n;\\
    4.42 +\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
    4.43 +\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
    4.44 +\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
    4.45  \hspace*{0pt}\\
    4.46  \hspace*{0pt}class Semigroup a where {\char123}\\
    4.47  \hspace*{0pt} ~mult ::~a -> a -> a;\\
    4.48  \hspace*{0pt}{\char125};\\
    4.49  \hspace*{0pt}\\
    4.50 -\hspace*{0pt}class (Example.Semigroup a) => Monoid a where {\char123}\\
    4.51 +\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
    4.52  \hspace*{0pt} ~neutral ::~a;\\
    4.53  \hspace*{0pt}{\char125};\\
    4.54  \hspace*{0pt}\\
    4.55 -\hspace*{0pt}pow ::~forall a.~(Example.Monoid a) => Example.Nat -> a -> a;\\
    4.56 -\hspace*{0pt}pow Example.Zero{\char95}nat a = Example.neutral;\\
    4.57 -\hspace*{0pt}pow (Example.Suc n) a = Example.mult a (Example.pow n a);\\
    4.58 +\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
    4.59 +\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
    4.60 +\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
    4.61  \hspace*{0pt}\\
    4.62 -\hspace*{0pt}mult{\char95}nat ::~Example.Nat -> Example.Nat -> Example.Nat;\\
    4.63 -\hspace*{0pt}mult{\char95}nat Example.Zero{\char95}nat n = Example.Zero{\char95}nat;\\
    4.64 -\hspace*{0pt}mult{\char95}nat (Example.Suc m) n = Example.plus{\char95}nat n (Example.mult{\char95}nat m n);\\
    4.65 +\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
    4.66 +\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
    4.67 +\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
    4.68  \hspace*{0pt}\\
    4.69 -\hspace*{0pt}neutral{\char95}nat ::~Example.Nat;\\
    4.70 -\hspace*{0pt}neutral{\char95}nat = Example.Suc Example.Zero{\char95}nat;\\
    4.71 -\hspace*{0pt}\\
    4.72 -\hspace*{0pt}instance Example.Semigroup Example.Nat where {\char123}\\
    4.73 -\hspace*{0pt} ~mult = Example.mult{\char95}nat;\\
    4.74 +\hspace*{0pt}instance Semigroup Nat where {\char123}\\
    4.75 +\hspace*{0pt} ~mult = mult{\char95}nat;\\
    4.76  \hspace*{0pt}{\char125};\\
    4.77  \hspace*{0pt}\\
    4.78 -\hspace*{0pt}instance Example.Monoid Example.Nat where {\char123}\\
    4.79 -\hspace*{0pt} ~neutral = Example.neutral{\char95}nat;\\
    4.80 +\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
    4.81 +\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
    4.82 +\hspace*{0pt}\\
    4.83 +\hspace*{0pt}instance Monoid Nat where {\char123}\\
    4.84 +\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
    4.85  \hspace*{0pt}{\char125};\\
    4.86  \hspace*{0pt}\\
    4.87 -\hspace*{0pt}bexp ::~Example.Nat -> Example.Nat;\\
    4.88 -\hspace*{0pt}bexp n = Example.pow n (Example.Suc (Example.Suc Example.Zero{\char95}nat));\\
    4.89 +\hspace*{0pt}bexp ::~Nat -> Nat;\\
    4.90 +\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
    4.91  \hspace*{0pt}\\
    4.92  \hspace*{0pt}{\char125}%
    4.93  \end{isamarkuptext}%

     5.1 --- a/doc-src/Codegen/Thy/document/Refinement.tex	Tue Sep 07 16:49:32 2010 +0200
     5.2 +++ b/doc-src/Codegen/Thy/document/Refinement.tex	Tue Sep 07 16:58:01 2010 +0200
     5.3 @@ -74,11 +74,10 @@
     5.4  \begin{isamarkuptext}%
     5.5  \isatypewriter%
     5.6  \noindent%
     5.7 -\hspace*{0pt}fib ::~Example.Nat -> Example.Nat;\\
     5.8 -\hspace*{0pt}fib Example.Zero{\char95}nat = Example.Zero{\char95}nat;\\
     5.9 -\hspace*{0pt}fib (Example.Suc Example.Zero{\char95}nat) = Example.Suc Example.Zero{\char95}nat;\\
    5.10 -\hspace*{0pt}fib (Example.Suc (Example.Suc n)) =\\
    5.11 -\hspace*{0pt} ~Example.plus{\char95}nat (Example.fib n) (Example.fib (Example.Suc n));%
    5.12 +\hspace*{0pt}fib ::~Nat -> Nat;\\
    5.13 +\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;\\
    5.14 +\hspace*{0pt}fib (Suc Zero{\char95}nat) = Suc Zero{\char95}nat;\\
    5.15 +\hspace*{0pt}fib (Suc (Suc n)) = plus{\char95}nat (fib n) (fib (Suc n));%
    5.16  \end{isamarkuptext}%
    5.17  \isamarkuptrue%
    5.18  %
    5.19 @@ -173,17 +172,15 @@
    5.20  \begin{isamarkuptext}%
    5.21  \isatypewriter%
    5.22  \noindent%
    5.23 -\hspace*{0pt}fib{\char95}step ::~Example.Nat -> (Example.Nat,~Example.Nat);\\
    5.24 -\hspace*{0pt}fib{\char95}step (Example.Suc n) =\\
    5.25 -\hspace*{0pt} ~let {\char123}\\
    5.26 -\hspace*{0pt} ~~~(m,~q) = Example.fib{\char95}step n;\\
    5.27 -\hspace*{0pt} ~{\char125}~in (Example.plus{\char95}nat m q,~m);\\
    5.28 -\hspace*{0pt}fib{\char95}step Example.Zero{\char95}nat =\\
    5.29 -\hspace*{0pt} ~(Example.Suc Example.Zero{\char95}nat,~Example.Zero{\char95}nat);\\
    5.30 +\hspace*{0pt}fib{\char95}step ::~Nat -> (Nat,~Nat);\\
    5.31 +\hspace*{0pt}fib{\char95}step (Suc n) = let {\char123}\\
    5.32 +\hspace*{0pt} ~~~~~~~~~~~~~~~~~~~~(m,~q) = fib{\char95}step n;\\
    5.33 +\hspace*{0pt} ~~~~~~~~~~~~~~~~~~{\char125}~in (plus{\char95}nat m q,~m);\\
    5.34 +\hspace*{0pt}fib{\char95}step Zero{\char95}nat = (Suc Zero{\char95}nat,~Zero{\char95}nat);\\
    5.35  \hspace*{0pt}\\
    5.36 -\hspace*{0pt}fib ::~Example.Nat -> Example.Nat;\\
    5.37 -\hspace*{0pt}fib (Example.Suc n) = fst (Example.fib{\char95}step n);\\
    5.38 -\hspace*{0pt}fib Example.Zero{\char95}nat = Example.Zero{\char95}nat;%
    5.39 +\hspace*{0pt}fib ::~Nat -> Nat;\\
    5.40 +\hspace*{0pt}fib (Suc n) = fst (fib{\char95}step n);\\
    5.41 +\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;%
    5.42  \end{isamarkuptext}%
    5.43  \isamarkuptrue%
    5.44  %
    5.45 @@ -593,30 +590,28 @@
    5.46  \hspace*{0pt}\\
    5.47  \hspace*{0pt}newtype Dlist a = Dlist [a];\\
    5.48  \hspace*{0pt}\\
    5.49 -\hspace*{0pt}empty ::~forall a.~Example.Dlist a;\\
    5.50 -\hspace*{0pt}empty = Example.Dlist [];\\
    5.51 +\hspace*{0pt}empty ::~forall a.~Dlist a;\\
    5.52 +\hspace*{0pt}empty = Dlist [];\\
    5.53  \hspace*{0pt}\\
    5.54  \hspace*{0pt}member ::~forall a.~(Eq a) => [a] -> a -> Bool;\\
    5.55  \hspace*{0pt}member [] y = False;\\
    5.56 -\hspace*{0pt}member (x :~xs) y = x == y || Example.member xs y;\\
    5.57 +\hspace*{0pt}member (x :~xs) y = x == y || member xs y;\\
    5.58  \hspace*{0pt}\\
    5.59 -\hspace*{0pt}inserta ::~forall a.~(Eq a) => a -> [a] -> [a];\\
    5.60 -\hspace*{0pt}inserta x xs = (if Example.member xs x then xs else x :~xs);\\
    5.61 +\hspace*{0pt}insert ::~forall a.~(Eq a) => a -> [a] -> [a];\\
    5.62 +\hspace*{0pt}insert x xs = (if member xs x then xs else x :~xs);\\
    5.63  \hspace*{0pt}\\
    5.64 -\hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Example.Dlist a -> [a];\\
    5.65 -\hspace*{0pt}list{\char95}of{\char95}dlist (Example.Dlist x) = x;\\
    5.66 +\hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Dlist a -> [a];\\
    5.67 +\hspace*{0pt}list{\char95}of{\char95}dlist (Dlist x) = x;\\
    5.68  \hspace*{0pt}\\
    5.69 -\hspace*{0pt}insert ::~forall a.~(Eq a) => a -> Example.Dlist a -> Example.Dlist a;\\
    5.70 -\hspace*{0pt}insert x dxs =\\
    5.71 -\hspace*{0pt} ~Example.Dlist (Example.inserta x (Example.list{\char95}of{\char95}dlist dxs));\\
    5.72 +\hspace*{0pt}inserta ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\
    5.73 +\hspace*{0pt}inserta x dxs = Dlist (insert x (list{\char95}of{\char95}dlist dxs));\\
    5.74  \hspace*{0pt}\\
    5.75  \hspace*{0pt}remove1 ::~forall a.~(Eq a) => a -> [a] -> [a];\\
    5.76  \hspace*{0pt}remove1 x [] = [];\\
    5.77 -\hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~Example.remove1 x xs);\\
    5.78 +\hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~remove1 x xs);\\
    5.79  \hspace*{0pt}\\
    5.80 -\hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Example.Dlist a -> Example.Dlist a;\\
    5.81 -\hspace*{0pt}remove x dxs =\\
    5.82 -\hspace*{0pt} ~Example.Dlist (Example.remove1 x (Example.list{\char95}of{\char95}dlist dxs));\\
    5.83 +\hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\
    5.84 +\hspace*{0pt}remove x dxs = Dlist (remove1 x (list{\char95}of{\char95}dlist dxs));\\
    5.85  \hspace*{0pt}\\
    5.86  \hspace*{0pt}{\char125}%
    5.87  \end{isamarkuptext}%

     6.1 --- a/doc-src/Codegen/Thy/examples/Example.hs	Tue Sep 07 16:49:32 2010 +0200
     6.2 +++ b/doc-src/Codegen/Thy/examples/Example.hs	Tue Sep 07 16:58:01 2010 +0200
     6.3 @@ -4,18 +4,18 @@
     6.4  
     6.5  data Queue a = AQueue [a] [a];
     6.6  
     6.7 -empty :: forall a. Example.Queue a;
     6.8 -empty = Example.AQueue [] [];
     6.9 +empty :: forall a. Queue a;
    6.10 +empty = AQueue [] [];
    6.11  
    6.12 -dequeue :: forall a. Example.Queue a -> (Maybe a, Example.Queue a);
    6.13 -dequeue (Example.AQueue [] []) = (Nothing, Example.AQueue [] []);
    6.14 -dequeue (Example.AQueue xs (y : ys)) = (Just y, Example.AQueue xs ys);
    6.15 -dequeue (Example.AQueue (v : va) []) =
    6.16 +dequeue :: forall a. Queue a -> (Maybe a, Queue a);
    6.17 +dequeue (AQueue [] []) = (Nothing, AQueue [] []);
    6.18 +dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys);
    6.19 +dequeue (AQueue (v : va) []) =
    6.20    let {
    6.21      (y : ys) = reverse (v : va);
    6.22 -  } in (Just y, Example.AQueue [] ys);
    6.23 +  } in (Just y, AQueue [] ys);
    6.24  
    6.25 -enqueue :: forall a. a -> Example.Queue a -> Example.Queue a;
    6.26 -enqueue x (Example.AQueue xs ys) = Example.AQueue (x : xs) ys;
    6.27 +enqueue :: forall a. a -> Queue a -> Queue a;
    6.28 +enqueue x (AQueue xs ys) = AQueue (x : xs) ys;
    6.29  
    6.30  }