--- a/doc-src/Classes/Thy/document/Classes.tex Thu Sep 02 15:09:51 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Thu Sep 02 16:14:09 2010 +0200
@@ -1134,26 +1134,27 @@
\noindent%
\hspace*{0pt}module Example where {\char123}\\
\hspace*{0pt}\\
-\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
+\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Example.Nat;\\
\hspace*{0pt}\\
-\hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
-\hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
+\hspace*{0pt}nat{\char95}aux ::~Integer -> Example.Nat -> Example.Nat;\\
+\hspace*{0pt}nat{\char95}aux i n =\\
+\hspace*{0pt} ~(if i <= 0 then n else Example.nat{\char95}aux (i - 1) (Example.Suc n));\\
\hspace*{0pt}\\
-\hspace*{0pt}nat ::~Integer -> Nat;\\
-\hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\
+\hspace*{0pt}nat ::~Integer -> Example.Nat;\\
+\hspace*{0pt}nat i = Example.nat{\char95}aux i Example.Zero{\char95}nat;\\
\hspace*{0pt}\\
\hspace*{0pt}class Semigroup a where {\char123}\\
\hspace*{0pt} ~mult ::~a -> a -> a;\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\
+\hspace*{0pt}class (Example.Semigroup a) => Monoidl a where {\char123}\\
\hspace*{0pt} ~neutral ::~a;\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\
+\hspace*{0pt}class (Example.Monoidl a) => Monoid a where {\char123}\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}class (Monoid a) => Group a where {\char123}\\
+\hspace*{0pt}class (Example.Monoid a) => Group a where {\char123}\\
\hspace*{0pt} ~inverse ::~a -> a;\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
@@ -1166,32 +1167,32 @@
\hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\
\hspace*{0pt}inverse{\char95}int i = negate i;\\
\hspace*{0pt}\\
-\hspace*{0pt}instance Semigroup Integer where {\char123}\\
-\hspace*{0pt} ~mult = mult{\char95}int;\\
+\hspace*{0pt}instance Example.Semigroup Integer where {\char123}\\
+\hspace*{0pt} ~mult = Example.mult{\char95}int;\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}instance Monoidl Integer where {\char123}\\
-\hspace*{0pt} ~neutral = neutral{\char95}int;\\
+\hspace*{0pt}instance Example.Monoidl Integer where {\char123}\\
+\hspace*{0pt} ~neutral = Example.neutral{\char95}int;\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}instance Monoid Integer where {\char123}\\
+\hspace*{0pt}instance Example.Monoid Integer where {\char123}\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}instance Group Integer where {\char123}\\
-\hspace*{0pt} ~inverse = inverse{\char95}int;\\
+\hspace*{0pt}instance Example.Group Integer where {\char123}\\
+\hspace*{0pt} ~inverse = Example.inverse{\char95}int;\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
-\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
-\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
+\hspace*{0pt}pow{\char95}nat ::~forall a.~(Example.Monoid a) => Example.Nat -> a -> a;\\
+\hspace*{0pt}pow{\char95}nat Example.Zero{\char95}nat x = Example.neutral;\\
+\hspace*{0pt}pow{\char95}nat (Example.Suc n) x = Example.mult x (Example.pow{\char95}nat n x);\\
\hspace*{0pt}\\
-\hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
+\hspace*{0pt}pow{\char95}int ::~forall a.~(Example.Group a) => Integer -> a -> a;\\
\hspace*{0pt}pow{\char95}int k x =\\
-\hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\
-\hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\
+\hspace*{0pt} ~(if 0 <= k then Example.pow{\char95}nat (Example.nat k) x\\
+\hspace*{0pt} ~~~else Example.inverse (Example.pow{\char95}nat (Example.nat (negate k)) x));\\
\hspace*{0pt}\\
\hspace*{0pt}example ::~Integer;\\
-\hspace*{0pt}example = pow{\char95}int 10 (-2);\\
+\hspace*{0pt}example = Example.pow{\char95}int 10 (-2);\\
\hspace*{0pt}\\
\hspace*{0pt}{\char125}%
\end{isamarkuptext}%
@@ -1232,15 +1233,15 @@
\hspace*{0pt} ~type 'a group\\
\hspace*{0pt} ~val monoid{\char95}group :~'a group -> 'a monoid\\
\hspace*{0pt} ~val inverse :~'a group -> 'a -> 'a\\
+\hspace*{0pt} ~val pow{\char95}nat :~'a monoid -> nat -> 'a -> 'a\\
+\hspace*{0pt} ~val pow{\char95}int :~'a group -> IntInf.int -> 'a -> 'a\\
\hspace*{0pt} ~val mult{\char95}int :~IntInf.int -> IntInf.int -> IntInf.int\\
+\hspace*{0pt} ~val semigroup{\char95}int :~IntInf.int semigroup\\
\hspace*{0pt} ~val neutral{\char95}int :~IntInf.int\\
-\hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\
-\hspace*{0pt} ~val semigroup{\char95}int :~IntInf.int semigroup\\
\hspace*{0pt} ~val monoidl{\char95}int :~IntInf.int monoidl\\
\hspace*{0pt} ~val monoid{\char95}int :~IntInf.int monoid\\
+\hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\
\hspace*{0pt} ~val group{\char95}int :~IntInf.int group\\
-\hspace*{0pt} ~val pow{\char95}nat :~'a monoid -> nat -> 'a -> 'a\\
-\hspace*{0pt} ~val pow{\char95}int :~'a group -> IntInf.int -> 'a -> 'a\\
\hspace*{0pt} ~val example :~IntInf.int\\
\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
@@ -1266,23 +1267,6 @@
\hspace*{0pt}val monoid{\char95}group = {\char35}monoid{\char95}group :~'a group -> 'a monoid;\\
\hspace*{0pt}val inverse = {\char35}inverse :~'a group -> 'a -> 'a;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\
-\hspace*{0pt}\\
-\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val monoidl{\char95}int =\\
-\hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
-\hspace*{0pt} ~IntInf.int monoidl;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
-\hspace*{0pt} ~IntInf.int group;\\
-\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
@@ -1292,6 +1276,23 @@
\hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\
\hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\
\hspace*{0pt}\\
+\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\
+\hspace*{0pt}\\
+\hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\
+\hspace*{0pt}\\
+\hspace*{0pt}val monoidl{\char95}int =\\
+\hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
+\hspace*{0pt} ~IntInf.int monoidl;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
+\hspace*{0pt} ~IntInf.int group;\\
+\hspace*{0pt}\\
\hspace*{0pt}val example :~IntInf.int =\\
\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\
\hspace*{0pt}\\
@@ -1335,9 +1336,6 @@
\noindent%
\hspace*{0pt}object Example {\char123}\\
\hspace*{0pt}\\
-\hspace*{0pt}import /*implicits*/ Example.semigroup{\char95}int,~Example.monoidl{\char95}int,\\
-\hspace*{0pt} ~Example.monoid{\char95}int,~Example.group{\char95}int\\
-\hspace*{0pt}\\
\hspace*{0pt}abstract sealed class nat\\
\hspace*{0pt}final case object Zero{\char95}nat extends nat\\
\hspace*{0pt}final case class Suc(a:~nat) extends nat\\
@@ -1348,23 +1346,23 @@
\hspace*{0pt}def nat(i:~BigInt):~nat = nat{\char95}aux(i,~Zero{\char95}nat)\\
\hspace*{0pt}\\
\hspace*{0pt}trait semigroup[A] {\char123}\\
-\hspace*{0pt} ~val `Example+mult`:~(A,~A) => A\\
+\hspace*{0pt} ~val `Example.mult`:~(A,~A) => A\\
\hspace*{0pt}{\char125}\\
\hspace*{0pt}def mult[A](a:~A,~b:~A)(implicit A:~semigroup[A]):~A =\\
-\hspace*{0pt} ~A.`Example+mult`(a,~b)\\
+\hspace*{0pt} ~A.`Example.mult`(a,~b)\\
\hspace*{0pt}\\
\hspace*{0pt}trait monoidl[A] extends semigroup[A] {\char123}\\
-\hspace*{0pt} ~val `Example+neutral`:~A\\
+\hspace*{0pt} ~val `Example.neutral`:~A\\
\hspace*{0pt}{\char125}\\
-\hspace*{0pt}def neutral[A](implicit A:~monoidl[A]):~A = A.`Example+neutral`\\
+\hspace*{0pt}def neutral[A](implicit A:~monoidl[A]):~A = A.`Example.neutral`\\
\hspace*{0pt}\\
\hspace*{0pt}trait monoid[A] extends monoidl[A] {\char123}\\
\hspace*{0pt}{\char125}\\
\hspace*{0pt}\\
\hspace*{0pt}trait group[A] extends monoid[A] {\char123}\\
-\hspace*{0pt} ~val `Example+inverse`:~A => A\\
+\hspace*{0pt} ~val `Example.inverse`:~A => A\\
\hspace*{0pt}{\char125}\\
-\hspace*{0pt}def inverse[A](a:~A)(implicit A:~group[A]):~A = A.`Example+inverse`(a)\\
+\hspace*{0pt}def inverse[A](a:~A)(implicit A:~group[A]):~A = A.`Example.inverse`(a)\\
\hspace*{0pt}\\
\hspace*{0pt}def pow{\char95}nat[A:~monoid](xa0:~nat,~x:~A):~A = (xa0,~x) match {\char123}\\
\hspace*{0pt} ~case (Zero{\char95}nat,~x) => neutral[A]\\
@@ -1378,27 +1376,27 @@
\hspace*{0pt}def mult{\char95}int(i:~BigInt,~j:~BigInt):~BigInt = i + j\\
\hspace*{0pt}\\
\hspace*{0pt}implicit def semigroup{\char95}int:~semigroup[BigInt] = new semigroup[BigInt] {\char123}\\
-\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
+\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
\hspace*{0pt}{\char125}\\
\hspace*{0pt}\\
\hspace*{0pt}def neutral{\char95}int:~BigInt = BigInt(0)\\
\hspace*{0pt}\\
\hspace*{0pt}implicit def monoidl{\char95}int:~monoidl[BigInt] = new monoidl[BigInt] {\char123}\\
-\hspace*{0pt} ~val `Example+neutral` = neutral{\char95}int\\
-\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
+\hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\
+\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
\hspace*{0pt}{\char125}\\
\hspace*{0pt}\\
\hspace*{0pt}implicit def monoid{\char95}int:~monoid[BigInt] = new monoid[BigInt] {\char123}\\
-\hspace*{0pt} ~val `Example+neutral` = neutral{\char95}int\\
-\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
+\hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\
+\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
\hspace*{0pt}{\char125}\\
\hspace*{0pt}\\
\hspace*{0pt}def inverse{\char95}int(i:~BigInt):~BigInt = (- i)\\
\hspace*{0pt}\\
\hspace*{0pt}implicit def group{\char95}int:~group[BigInt] = new group[BigInt] {\char123}\\
-\hspace*{0pt} ~val `Example+inverse` = (a:~BigInt) => inverse{\char95}int(a)\\
-\hspace*{0pt} ~val `Example+neutral` = neutral{\char95}int\\
-\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
+\hspace*{0pt} ~val `Example.inverse` = (a:~BigInt) => inverse{\char95}int(a)\\
+\hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\
+\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
\hspace*{0pt}{\char125}\\
\hspace*{0pt}\\
\hspace*{0pt}def example:~BigInt = pow{\char95}int[BigInt](BigInt(10),~BigInt(- 2))\\