1132 \begin{isamarkuptext}% |
1132 \begin{isamarkuptext}% |
1133 \isatypewriter% |
1133 \isatypewriter% |
1134 \noindent% |
1134 \noindent% |
1135 \hspace*{0pt}module Example where {\char123}\\ |
1135 \hspace*{0pt}module Example where {\char123}\\ |
1136 \hspace*{0pt}\\ |
1136 \hspace*{0pt}\\ |
1137 \hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\ |
1137 \hspace*{0pt}data Nat = Zero{\char95}nat | Suc Example.Nat;\\ |
1138 \hspace*{0pt}\\ |
1138 \hspace*{0pt}\\ |
1139 \hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\ |
1139 \hspace*{0pt}nat{\char95}aux ::~Integer -> Example.Nat -> Example.Nat;\\ |
1140 \hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\ |
1140 \hspace*{0pt}nat{\char95}aux i n =\\ |
1141 \hspace*{0pt}\\ |
1141 \hspace*{0pt} ~(if i <= 0 then n else Example.nat{\char95}aux (i - 1) (Example.Suc n));\\ |
1142 \hspace*{0pt}nat ::~Integer -> Nat;\\ |
1142 \hspace*{0pt}\\ |
1143 \hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\ |
1143 \hspace*{0pt}nat ::~Integer -> Example.Nat;\\ |
|
1144 \hspace*{0pt}nat i = Example.nat{\char95}aux i Example.Zero{\char95}nat;\\ |
1144 \hspace*{0pt}\\ |
1145 \hspace*{0pt}\\ |
1145 \hspace*{0pt}class Semigroup a where {\char123}\\ |
1146 \hspace*{0pt}class Semigroup a where {\char123}\\ |
1146 \hspace*{0pt} ~mult ::~a -> a -> a;\\ |
1147 \hspace*{0pt} ~mult ::~a -> a -> a;\\ |
1147 \hspace*{0pt}{\char125};\\ |
1148 \hspace*{0pt}{\char125};\\ |
1148 \hspace*{0pt}\\ |
1149 \hspace*{0pt}\\ |
1149 \hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\ |
1150 \hspace*{0pt}class (Example.Semigroup a) => Monoidl a where {\char123}\\ |
1150 \hspace*{0pt} ~neutral ::~a;\\ |
1151 \hspace*{0pt} ~neutral ::~a;\\ |
1151 \hspace*{0pt}{\char125};\\ |
1152 \hspace*{0pt}{\char125};\\ |
1152 \hspace*{0pt}\\ |
1153 \hspace*{0pt}\\ |
1153 \hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\ |
1154 \hspace*{0pt}class (Example.Monoidl a) => Monoid a where {\char123}\\ |
1154 \hspace*{0pt}{\char125};\\ |
1155 \hspace*{0pt}{\char125};\\ |
1155 \hspace*{0pt}\\ |
1156 \hspace*{0pt}\\ |
1156 \hspace*{0pt}class (Monoid a) => Group a where {\char123}\\ |
1157 \hspace*{0pt}class (Example.Monoid a) => Group a where {\char123}\\ |
1157 \hspace*{0pt} ~inverse ::~a -> a;\\ |
1158 \hspace*{0pt} ~inverse ::~a -> a;\\ |
1158 \hspace*{0pt}{\char125};\\ |
1159 \hspace*{0pt}{\char125};\\ |
1159 \hspace*{0pt}\\ |
1160 \hspace*{0pt}\\ |
1160 \hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\ |
1161 \hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\ |
1161 \hspace*{0pt}mult{\char95}int i j = i + j;\\ |
1162 \hspace*{0pt}mult{\char95}int i j = i + j;\\ |
1164 \hspace*{0pt}neutral{\char95}int = 0;\\ |
1165 \hspace*{0pt}neutral{\char95}int = 0;\\ |
1165 \hspace*{0pt}\\ |
1166 \hspace*{0pt}\\ |
1166 \hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\ |
1167 \hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\ |
1167 \hspace*{0pt}inverse{\char95}int i = negate i;\\ |
1168 \hspace*{0pt}inverse{\char95}int i = negate i;\\ |
1168 \hspace*{0pt}\\ |
1169 \hspace*{0pt}\\ |
1169 \hspace*{0pt}instance Semigroup Integer where {\char123}\\ |
1170 \hspace*{0pt}instance Example.Semigroup Integer where {\char123}\\ |
1170 \hspace*{0pt} ~mult = mult{\char95}int;\\ |
1171 \hspace*{0pt} ~mult = Example.mult{\char95}int;\\ |
1171 \hspace*{0pt}{\char125};\\ |
1172 \hspace*{0pt}{\char125};\\ |
1172 \hspace*{0pt}\\ |
1173 \hspace*{0pt}\\ |
1173 \hspace*{0pt}instance Monoidl Integer where {\char123}\\ |
1174 \hspace*{0pt}instance Example.Monoidl Integer where {\char123}\\ |
1174 \hspace*{0pt} ~neutral = neutral{\char95}int;\\ |
1175 \hspace*{0pt} ~neutral = Example.neutral{\char95}int;\\ |
1175 \hspace*{0pt}{\char125};\\ |
1176 \hspace*{0pt}{\char125};\\ |
1176 \hspace*{0pt}\\ |
1177 \hspace*{0pt}\\ |
1177 \hspace*{0pt}instance Monoid Integer where {\char123}\\ |
1178 \hspace*{0pt}instance Example.Monoid Integer where {\char123}\\ |
1178 \hspace*{0pt}{\char125};\\ |
1179 \hspace*{0pt}{\char125};\\ |
1179 \hspace*{0pt}\\ |
1180 \hspace*{0pt}\\ |
1180 \hspace*{0pt}instance Group Integer where {\char123}\\ |
1181 \hspace*{0pt}instance Example.Group Integer where {\char123}\\ |
1181 \hspace*{0pt} ~inverse = inverse{\char95}int;\\ |
1182 \hspace*{0pt} ~inverse = Example.inverse{\char95}int;\\ |
1182 \hspace*{0pt}{\char125};\\ |
1183 \hspace*{0pt}{\char125};\\ |
1183 \hspace*{0pt}\\ |
1184 \hspace*{0pt}\\ |
1184 \hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\ |
1185 \hspace*{0pt}pow{\char95}nat ::~forall a.~(Example.Monoid a) => Example.Nat -> a -> a;\\ |
1185 \hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\ |
1186 \hspace*{0pt}pow{\char95}nat Example.Zero{\char95}nat x = Example.neutral;\\ |
1186 \hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\ |
1187 \hspace*{0pt}pow{\char95}nat (Example.Suc n) x = Example.mult x (Example.pow{\char95}nat n x);\\ |
1187 \hspace*{0pt}\\ |
1188 \hspace*{0pt}\\ |
1188 \hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\ |
1189 \hspace*{0pt}pow{\char95}int ::~forall a.~(Example.Group a) => Integer -> a -> a;\\ |
1189 \hspace*{0pt}pow{\char95}int k x =\\ |
1190 \hspace*{0pt}pow{\char95}int k x =\\ |
1190 \hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\ |
1191 \hspace*{0pt} ~(if 0 <= k then Example.pow{\char95}nat (Example.nat k) x\\ |
1191 \hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\ |
1192 \hspace*{0pt} ~~~else Example.inverse (Example.pow{\char95}nat (Example.nat (negate k)) x));\\ |
1192 \hspace*{0pt}\\ |
1193 \hspace*{0pt}\\ |
1193 \hspace*{0pt}example ::~Integer;\\ |
1194 \hspace*{0pt}example ::~Integer;\\ |
1194 \hspace*{0pt}example = pow{\char95}int 10 (-2);\\ |
1195 \hspace*{0pt}example = Example.pow{\char95}int 10 (-2);\\ |
1195 \hspace*{0pt}\\ |
1196 \hspace*{0pt}\\ |
1196 \hspace*{0pt}{\char125}% |
1197 \hspace*{0pt}{\char125}% |
1197 \end{isamarkuptext}% |
1198 \end{isamarkuptext}% |
1198 \isamarkuptrue% |
1199 \isamarkuptrue% |
1199 % |
1200 % |
1230 \hspace*{0pt} ~type 'a monoid\\ |
1231 \hspace*{0pt} ~type 'a monoid\\ |
1231 \hspace*{0pt} ~val monoidl{\char95}monoid :~'a monoid -> 'a monoidl\\ |
1232 \hspace*{0pt} ~val monoidl{\char95}monoid :~'a monoid -> 'a monoidl\\ |
1232 \hspace*{0pt} ~type 'a group\\ |
1233 \hspace*{0pt} ~type 'a group\\ |
1233 \hspace*{0pt} ~val monoid{\char95}group :~'a group -> 'a monoid\\ |
1234 \hspace*{0pt} ~val monoid{\char95}group :~'a group -> 'a monoid\\ |
1234 \hspace*{0pt} ~val inverse :~'a group -> 'a -> 'a\\ |
1235 \hspace*{0pt} ~val inverse :~'a group -> 'a -> 'a\\ |
|
1236 \hspace*{0pt} ~val pow{\char95}nat :~'a monoid -> nat -> 'a -> 'a\\ |
|
1237 \hspace*{0pt} ~val pow{\char95}int :~'a group -> IntInf.int -> 'a -> 'a\\ |
1235 \hspace*{0pt} ~val mult{\char95}int :~IntInf.int -> IntInf.int -> IntInf.int\\ |
1238 \hspace*{0pt} ~val mult{\char95}int :~IntInf.int -> IntInf.int -> IntInf.int\\ |
|
1239 \hspace*{0pt} ~val semigroup{\char95}int :~IntInf.int semigroup\\ |
1236 \hspace*{0pt} ~val neutral{\char95}int :~IntInf.int\\ |
1240 \hspace*{0pt} ~val neutral{\char95}int :~IntInf.int\\ |
1237 \hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\ |
|
1238 \hspace*{0pt} ~val semigroup{\char95}int :~IntInf.int semigroup\\ |
|
1239 \hspace*{0pt} ~val monoidl{\char95}int :~IntInf.int monoidl\\ |
1241 \hspace*{0pt} ~val monoidl{\char95}int :~IntInf.int monoidl\\ |
1240 \hspace*{0pt} ~val monoid{\char95}int :~IntInf.int monoid\\ |
1242 \hspace*{0pt} ~val monoid{\char95}int :~IntInf.int monoid\\ |
|
1243 \hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\ |
1241 \hspace*{0pt} ~val group{\char95}int :~IntInf.int group\\ |
1244 \hspace*{0pt} ~val group{\char95}int :~IntInf.int group\\ |
1242 \hspace*{0pt} ~val pow{\char95}nat :~'a monoid -> nat -> 'a -> 'a\\ |
|
1243 \hspace*{0pt} ~val pow{\char95}int :~'a group -> IntInf.int -> 'a -> 'a\\ |
|
1244 \hspace*{0pt} ~val example :~IntInf.int\\ |
1245 \hspace*{0pt} ~val example :~IntInf.int\\ |
1245 \hspace*{0pt}end = struct\\ |
1246 \hspace*{0pt}end = struct\\ |
1246 \hspace*{0pt}\\ |
1247 \hspace*{0pt}\\ |
1247 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ |
1248 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ |
1248 \hspace*{0pt}\\ |
1249 \hspace*{0pt}\\ |
1263 \hspace*{0pt}val monoidl{\char95}monoid = {\char35}monoidl{\char95}monoid :~'a monoid -> 'a monoidl;\\ |
1264 \hspace*{0pt}val monoidl{\char95}monoid = {\char35}monoidl{\char95}monoid :~'a monoid -> 'a monoidl;\\ |
1264 \hspace*{0pt}\\ |
1265 \hspace*{0pt}\\ |
1265 \hspace*{0pt}type 'a group = {\char123}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\ |
1266 \hspace*{0pt}type 'a group = {\char123}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\ |
1266 \hspace*{0pt}val monoid{\char95}group = {\char35}monoid{\char95}group :~'a group -> 'a monoid;\\ |
1267 \hspace*{0pt}val monoid{\char95}group = {\char35}monoid{\char95}group :~'a group -> 'a monoid;\\ |
1267 \hspace*{0pt}val inverse = {\char35}inverse :~'a group -> 'a -> 'a;\\ |
1268 \hspace*{0pt}val inverse = {\char35}inverse :~'a group -> 'a -> 'a;\\ |
1268 \hspace*{0pt}\\ |
|
1269 \hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\ |
|
1270 \hspace*{0pt}\\ |
|
1271 \hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\ |
|
1272 \hspace*{0pt}\\ |
|
1273 \hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\ |
|
1274 \hspace*{0pt}\\ |
|
1275 \hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\ |
|
1276 \hspace*{0pt}\\ |
|
1277 \hspace*{0pt}val monoidl{\char95}int =\\ |
|
1278 \hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\ |
|
1279 \hspace*{0pt} ~IntInf.int monoidl;\\ |
|
1280 \hspace*{0pt}\\ |
|
1281 \hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\ |
|
1282 \hspace*{0pt}\\ |
|
1283 \hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\ |
|
1284 \hspace*{0pt} ~IntInf.int group;\\ |
|
1285 \hspace*{0pt}\\ |
1269 \hspace*{0pt}\\ |
1286 \hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\ |
1270 \hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\ |
1287 \hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\ |
1271 \hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\ |
1288 \hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\ |
1272 \hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\ |
1289 \hspace*{0pt}\\ |
1273 \hspace*{0pt}\\ |
1290 \hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\ |
1274 \hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\ |
1291 \hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\ |
1275 \hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\ |
1292 \hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\ |
1276 \hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\ |
1293 \hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\ |
1277 \hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\ |
1294 \hspace*{0pt}\\ |
1278 \hspace*{0pt}\\ |
|
1279 \hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\ |
|
1280 \hspace*{0pt}\\ |
|
1281 \hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\ |
|
1282 \hspace*{0pt}\\ |
|
1283 \hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\ |
|
1284 \hspace*{0pt}\\ |
|
1285 \hspace*{0pt}val monoidl{\char95}int =\\ |
|
1286 \hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\ |
|
1287 \hspace*{0pt} ~IntInf.int monoidl;\\ |
|
1288 \hspace*{0pt}\\ |
|
1289 \hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\ |
|
1290 \hspace*{0pt}\\ |
|
1291 \hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\ |
|
1292 \hspace*{0pt}\\ |
|
1293 \hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\ |
|
1294 \hspace*{0pt} ~IntInf.int group;\\ |
|
1295 \hspace*{0pt}\\ |
1295 \hspace*{0pt}val example :~IntInf.int =\\ |
1296 \hspace*{0pt}val example :~IntInf.int =\\ |
1296 \hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\ |
1297 \hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\ |
1297 \hspace*{0pt}\\ |
1298 \hspace*{0pt}\\ |
1298 \hspace*{0pt}end;~(*struct Example*)% |
1299 \hspace*{0pt}end;~(*struct Example*)% |
1299 \end{isamarkuptext}% |
1300 \end{isamarkuptext}% |
1333 \begin{isamarkuptext}% |
1334 \begin{isamarkuptext}% |
1334 \isatypewriter% |
1335 \isatypewriter% |
1335 \noindent% |
1336 \noindent% |
1336 \hspace*{0pt}object Example {\char123}\\ |
1337 \hspace*{0pt}object Example {\char123}\\ |
1337 \hspace*{0pt}\\ |
1338 \hspace*{0pt}\\ |
1338 \hspace*{0pt}import /*implicits*/ Example.semigroup{\char95}int,~Example.monoidl{\char95}int,\\ |
|
1339 \hspace*{0pt} ~Example.monoid{\char95}int,~Example.group{\char95}int\\ |
|
1340 \hspace*{0pt}\\ |
|
1341 \hspace*{0pt}abstract sealed class nat\\ |
1339 \hspace*{0pt}abstract sealed class nat\\ |
1342 \hspace*{0pt}final case object Zero{\char95}nat extends nat\\ |
1340 \hspace*{0pt}final case object Zero{\char95}nat extends nat\\ |
1343 \hspace*{0pt}final case class Suc(a:~nat) extends nat\\ |
1341 \hspace*{0pt}final case class Suc(a:~nat) extends nat\\ |
1344 \hspace*{0pt}\\ |
1342 \hspace*{0pt}\\ |
1345 \hspace*{0pt}def nat{\char95}aux(i:~BigInt,~n:~nat):~nat =\\ |
1343 \hspace*{0pt}def nat{\char95}aux(i:~BigInt,~n:~nat):~nat =\\ |
1346 \hspace*{0pt} ~(if (i <= BigInt(0)) n else nat{\char95}aux(i - BigInt(1),~Suc(n)))\\ |
1344 \hspace*{0pt} ~(if (i <= BigInt(0)) n else nat{\char95}aux(i - BigInt(1),~Suc(n)))\\ |
1347 \hspace*{0pt}\\ |
1345 \hspace*{0pt}\\ |
1348 \hspace*{0pt}def nat(i:~BigInt):~nat = nat{\char95}aux(i,~Zero{\char95}nat)\\ |
1346 \hspace*{0pt}def nat(i:~BigInt):~nat = nat{\char95}aux(i,~Zero{\char95}nat)\\ |
1349 \hspace*{0pt}\\ |
1347 \hspace*{0pt}\\ |
1350 \hspace*{0pt}trait semigroup[A] {\char123}\\ |
1348 \hspace*{0pt}trait semigroup[A] {\char123}\\ |
1351 \hspace*{0pt} ~val `Example+mult`:~(A,~A) => A\\ |
1349 \hspace*{0pt} ~val `Example.mult`:~(A,~A) => A\\ |
1352 \hspace*{0pt}{\char125}\\ |
1350 \hspace*{0pt}{\char125}\\ |
1353 \hspace*{0pt}def mult[A](a:~A,~b:~A)(implicit A:~semigroup[A]):~A =\\ |
1351 \hspace*{0pt}def mult[A](a:~A,~b:~A)(implicit A:~semigroup[A]):~A =\\ |
1354 \hspace*{0pt} ~A.`Example+mult`(a,~b)\\ |
1352 \hspace*{0pt} ~A.`Example.mult`(a,~b)\\ |
1355 \hspace*{0pt}\\ |
1353 \hspace*{0pt}\\ |
1356 \hspace*{0pt}trait monoidl[A] extends semigroup[A] {\char123}\\ |
1354 \hspace*{0pt}trait monoidl[A] extends semigroup[A] {\char123}\\ |
1357 \hspace*{0pt} ~val `Example+neutral`:~A\\ |
1355 \hspace*{0pt} ~val `Example.neutral`:~A\\ |
1358 \hspace*{0pt}{\char125}\\ |
1356 \hspace*{0pt}{\char125}\\ |
1359 \hspace*{0pt}def neutral[A](implicit A:~monoidl[A]):~A = A.`Example+neutral`\\ |
1357 \hspace*{0pt}def neutral[A](implicit A:~monoidl[A]):~A = A.`Example.neutral`\\ |
1360 \hspace*{0pt}\\ |
1358 \hspace*{0pt}\\ |
1361 \hspace*{0pt}trait monoid[A] extends monoidl[A] {\char123}\\ |
1359 \hspace*{0pt}trait monoid[A] extends monoidl[A] {\char123}\\ |
1362 \hspace*{0pt}{\char125}\\ |
1360 \hspace*{0pt}{\char125}\\ |
1363 \hspace*{0pt}\\ |
1361 \hspace*{0pt}\\ |
1364 \hspace*{0pt}trait group[A] extends monoid[A] {\char123}\\ |
1362 \hspace*{0pt}trait group[A] extends monoid[A] {\char123}\\ |
1365 \hspace*{0pt} ~val `Example+inverse`:~A => A\\ |
1363 \hspace*{0pt} ~val `Example.inverse`:~A => A\\ |
1366 \hspace*{0pt}{\char125}\\ |
1364 \hspace*{0pt}{\char125}\\ |
1367 \hspace*{0pt}def inverse[A](a:~A)(implicit A:~group[A]):~A = A.`Example+inverse`(a)\\ |
1365 \hspace*{0pt}def inverse[A](a:~A)(implicit A:~group[A]):~A = A.`Example.inverse`(a)\\ |
1368 \hspace*{0pt}\\ |
1366 \hspace*{0pt}\\ |
1369 \hspace*{0pt}def pow{\char95}nat[A:~monoid](xa0:~nat,~x:~A):~A = (xa0,~x) match {\char123}\\ |
1367 \hspace*{0pt}def pow{\char95}nat[A:~monoid](xa0:~nat,~x:~A):~A = (xa0,~x) match {\char123}\\ |
1370 \hspace*{0pt} ~case (Zero{\char95}nat,~x) => neutral[A]\\ |
1368 \hspace*{0pt} ~case (Zero{\char95}nat,~x) => neutral[A]\\ |
1371 \hspace*{0pt} ~case (Suc(n),~x) => mult[A](x,~pow{\char95}nat[A](n,~x))\\ |
1369 \hspace*{0pt} ~case (Suc(n),~x) => mult[A](x,~pow{\char95}nat[A](n,~x))\\ |
1372 \hspace*{0pt}{\char125}\\ |
1370 \hspace*{0pt}{\char125}\\ |
1376 \hspace*{0pt} ~~~else inverse[A](pow{\char95}nat[A](nat((- k)),~x)))\\ |
1374 \hspace*{0pt} ~~~else inverse[A](pow{\char95}nat[A](nat((- k)),~x)))\\ |
1377 \hspace*{0pt}\\ |
1375 \hspace*{0pt}\\ |
1378 \hspace*{0pt}def mult{\char95}int(i:~BigInt,~j:~BigInt):~BigInt = i + j\\ |
1376 \hspace*{0pt}def mult{\char95}int(i:~BigInt,~j:~BigInt):~BigInt = i + j\\ |
1379 \hspace*{0pt}\\ |
1377 \hspace*{0pt}\\ |
1380 \hspace*{0pt}implicit def semigroup{\char95}int:~semigroup[BigInt] = new semigroup[BigInt] {\char123}\\ |
1378 \hspace*{0pt}implicit def semigroup{\char95}int:~semigroup[BigInt] = new semigroup[BigInt] {\char123}\\ |
1381 \hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ |
1379 \hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ |
1382 \hspace*{0pt}{\char125}\\ |
1380 \hspace*{0pt}{\char125}\\ |
1383 \hspace*{0pt}\\ |
1381 \hspace*{0pt}\\ |
1384 \hspace*{0pt}def neutral{\char95}int:~BigInt = BigInt(0)\\ |
1382 \hspace*{0pt}def neutral{\char95}int:~BigInt = BigInt(0)\\ |
1385 \hspace*{0pt}\\ |
1383 \hspace*{0pt}\\ |
1386 \hspace*{0pt}implicit def monoidl{\char95}int:~monoidl[BigInt] = new monoidl[BigInt] {\char123}\\ |
1384 \hspace*{0pt}implicit def monoidl{\char95}int:~monoidl[BigInt] = new monoidl[BigInt] {\char123}\\ |
1387 \hspace*{0pt} ~val `Example+neutral` = neutral{\char95}int\\ |
1385 \hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\ |
1388 \hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ |
1386 \hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ |
1389 \hspace*{0pt}{\char125}\\ |
1387 \hspace*{0pt}{\char125}\\ |
1390 \hspace*{0pt}\\ |
1388 \hspace*{0pt}\\ |
1391 \hspace*{0pt}implicit def monoid{\char95}int:~monoid[BigInt] = new monoid[BigInt] {\char123}\\ |
1389 \hspace*{0pt}implicit def monoid{\char95}int:~monoid[BigInt] = new monoid[BigInt] {\char123}\\ |
1392 \hspace*{0pt} ~val `Example+neutral` = neutral{\char95}int\\ |
1390 \hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\ |
1393 \hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ |
1391 \hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ |
1394 \hspace*{0pt}{\char125}\\ |
1392 \hspace*{0pt}{\char125}\\ |
1395 \hspace*{0pt}\\ |
1393 \hspace*{0pt}\\ |
1396 \hspace*{0pt}def inverse{\char95}int(i:~BigInt):~BigInt = (- i)\\ |
1394 \hspace*{0pt}def inverse{\char95}int(i:~BigInt):~BigInt = (- i)\\ |
1397 \hspace*{0pt}\\ |
1395 \hspace*{0pt}\\ |
1398 \hspace*{0pt}implicit def group{\char95}int:~group[BigInt] = new group[BigInt] {\char123}\\ |
1396 \hspace*{0pt}implicit def group{\char95}int:~group[BigInt] = new group[BigInt] {\char123}\\ |
1399 \hspace*{0pt} ~val `Example+inverse` = (a:~BigInt) => inverse{\char95}int(a)\\ |
1397 \hspace*{0pt} ~val `Example.inverse` = (a:~BigInt) => inverse{\char95}int(a)\\ |
1400 \hspace*{0pt} ~val `Example+neutral` = neutral{\char95}int\\ |
1398 \hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\ |
1401 \hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ |
1399 \hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ |
1402 \hspace*{0pt}{\char125}\\ |
1400 \hspace*{0pt}{\char125}\\ |
1403 \hspace*{0pt}\\ |
1401 \hspace*{0pt}\\ |
1404 \hspace*{0pt}def example:~BigInt = pow{\char95}int[BigInt](BigInt(10),~BigInt(- 2))\\ |
1402 \hspace*{0pt}def example:~BigInt = pow{\char95}int[BigInt](BigInt(10),~BigInt(- 2))\\ |
1405 \hspace*{0pt}\\ |
1403 \hspace*{0pt}\\ |
1406 \hspace*{0pt}{\char125}~/* object Example */% |
1404 \hspace*{0pt}{\char125}~/* object Example */% |