1.1 --- a/doc-src/Codegen/Thy/document/Introduction.tex	Tue Sep 07 16:49:32 2010 +0200
     1.2 +++ b/doc-src/Codegen/Thy/document/Introduction.tex	Tue Sep 07 16:58:01 2010 +0200
     1.3 @@ -231,19 +231,19 @@
     1.4  \hspace*{0pt}\\
     1.5  \hspace*{0pt}data Queue a = AQueue [a] [a];\\
     1.6  \hspace*{0pt}\\
     1.7 -\hspace*{0pt}empty ::~forall a.~Example.Queue a;\\
     1.8 -\hspace*{0pt}empty = Example.AQueue [] [];\\
     1.9 +\hspace*{0pt}empty ::~forall a.~Queue a;\\
    1.10 +\hspace*{0pt}empty = AQueue [] [];\\
    1.11  \hspace*{0pt}\\
    1.12 -\hspace*{0pt}dequeue ::~forall a.~Example.Queue a -> (Maybe a,~Example.Queue a);\\
    1.13 -\hspace*{0pt}dequeue (Example.AQueue [] []) = (Nothing,~Example.AQueue [] []);\\
    1.14 -\hspace*{0pt}dequeue (Example.AQueue xs (y :~ys)) = (Just y,~Example.AQueue xs ys);\\
    1.15 -\hspace*{0pt}dequeue (Example.AQueue (v :~va) []) =\\
    1.16 +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
    1.17 +\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\
    1.18 +\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
    1.19 +\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\
    1.20  \hspace*{0pt} ~let {\char123}\\
    1.21  \hspace*{0pt} ~~~(y :~ys) = reverse (v :~va);\\
    1.22 -\hspace*{0pt} ~{\char125}~in (Just y,~Example.AQueue [] ys);\\
    1.23 +\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
    1.24  \hspace*{0pt}\\
    1.25 -\hspace*{0pt}enqueue ::~forall a.~a -> Example.Queue a -> Example.Queue a;\\
    1.26 -\hspace*{0pt}enqueue x (Example.AQueue xs ys) = Example.AQueue (x :~xs) ys;\\
    1.27 +\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
    1.28 +\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
    1.29  \hspace*{0pt}\\
    1.30  \hspace*{0pt}{\char125}%
    1.31  \end{isamarkuptext}%
    1.32 @@ -397,41 +397,41 @@
    1.33  \noindent%
    1.34  \hspace*{0pt}module Example where {\char123}\\
    1.35  \hspace*{0pt}\\
    1.36 -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Example.Nat;\\
    1.37 +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
    1.38  \hspace*{0pt}\\
    1.39 -\hspace*{0pt}plus{\char95}nat ::~Example.Nat -> Example.Nat -> Example.Nat;\\
    1.40 -\hspace*{0pt}plus{\char95}nat (Example.Suc m) n = Example.plus{\char95}nat m (Example.Suc n);\\
    1.41 -\hspace*{0pt}plus{\char95}nat Example.Zero{\char95}nat n = n;\\
    1.42 +\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
    1.43 +\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
    1.44 +\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
    1.45  \hspace*{0pt}\\
    1.46  \hspace*{0pt}class Semigroup a where {\char123}\\
    1.47  \hspace*{0pt} ~mult ::~a -> a -> a;\\
    1.48  \hspace*{0pt}{\char125};\\
    1.49  \hspace*{0pt}\\
    1.50 -\hspace*{0pt}class (Example.Semigroup a) => Monoid a where {\char123}\\
    1.51 +\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
    1.52  \hspace*{0pt} ~neutral ::~a;\\
    1.53  \hspace*{0pt}{\char125};\\
    1.54  \hspace*{0pt}\\
    1.55 -\hspace*{0pt}pow ::~forall a.~(Example.Monoid a) => Example.Nat -> a -> a;\\
    1.56 -\hspace*{0pt}pow Example.Zero{\char95}nat a = Example.neutral;\\
    1.57 -\hspace*{0pt}pow (Example.Suc n) a = Example.mult a (Example.pow n a);\\
    1.58 +\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
    1.59 +\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
    1.60 +\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
    1.61  \hspace*{0pt}\\
    1.62 -\hspace*{0pt}mult{\char95}nat ::~Example.Nat -> Example.Nat -> Example.Nat;\\
    1.63 -\hspace*{0pt}mult{\char95}nat Example.Zero{\char95}nat n = Example.Zero{\char95}nat;\\
    1.64 -\hspace*{0pt}mult{\char95}nat (Example.Suc m) n = Example.plus{\char95}nat n (Example.mult{\char95}nat m n);\\
    1.65 +\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
    1.66 +\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
    1.67 +\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
    1.68  \hspace*{0pt}\\
    1.69 -\hspace*{0pt}neutral{\char95}nat ::~Example.Nat;\\
    1.70 -\hspace*{0pt}neutral{\char95}nat = Example.Suc Example.Zero{\char95}nat;\\
    1.71 -\hspace*{0pt}\\
    1.72 -\hspace*{0pt}instance Example.Semigroup Example.Nat where {\char123}\\
    1.73 -\hspace*{0pt} ~mult = Example.mult{\char95}nat;\\
    1.74 +\hspace*{0pt}instance Semigroup Nat where {\char123}\\
    1.75 +\hspace*{0pt} ~mult = mult{\char95}nat;\\
    1.76  \hspace*{0pt}{\char125};\\
    1.77  \hspace*{0pt}\\
    1.78 -\hspace*{0pt}instance Example.Monoid Example.Nat where {\char123}\\
    1.79 -\hspace*{0pt} ~neutral = Example.neutral{\char95}nat;\\
    1.80 +\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
    1.81 +\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
    1.82 +\hspace*{0pt}\\
    1.83 +\hspace*{0pt}instance Monoid Nat where {\char123}\\
    1.84 +\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
    1.85  \hspace*{0pt}{\char125};\\
    1.86  \hspace*{0pt}\\
    1.87 -\hspace*{0pt}bexp ::~Example.Nat -> Example.Nat;\\
    1.88 -\hspace*{0pt}bexp n = Example.pow n (Example.Suc (Example.Suc Example.Zero{\char95}nat));\\
    1.89 +\hspace*{0pt}bexp ::~Nat -> Nat;\\
    1.90 +\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
    1.91  \hspace*{0pt}\\
    1.92  \hspace*{0pt}{\char125}%
    1.93  \end{isamarkuptext}%