1164 \hspace*{0pt}\\ |
1164 \hspace*{0pt}\\ |
1165 \hspace*{0pt}instance Group Integer where {\char123}\\ |
1165 \hspace*{0pt}instance Group Integer where {\char123}\\ |
1166 \hspace*{0pt} ~inverse = inverse{\char95}int;\\ |
1166 \hspace*{0pt} ~inverse = inverse{\char95}int;\\ |
1167 \hspace*{0pt}{\char125};\\ |
1167 \hspace*{0pt}{\char125};\\ |
1168 \hspace*{0pt}\\ |
1168 \hspace*{0pt}\\ |
1169 \hspace*{0pt}pow{\char95}nat ::~forall a. (Monoid a) => Nat -> a -> a;\\ |
1169 \hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\ |
1170 \hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\ |
1170 \hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\ |
1171 \hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\ |
1171 \hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\ |
1172 \hspace*{0pt}\\ |
1172 \hspace*{0pt}\\ |
1173 \hspace*{0pt}pow{\char95}int ::~forall a. (Group a) => Integer -> a -> a;\\ |
1173 \hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\ |
1174 \hspace*{0pt}pow{\char95}int k x =\\ |
1174 \hspace*{0pt}pow{\char95}int k x =\\ |
1175 \hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\ |
1175 \hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\ |
1176 \hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\ |
1176 \hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\ |
1177 \hspace*{0pt}\\ |
1177 \hspace*{0pt}\\ |
1178 \hspace*{0pt}example ::~Integer;\\ |
1178 \hspace*{0pt}example ::~Integer;\\ |
1207 \hspace*{0pt}struct\\ |
1207 \hspace*{0pt}struct\\ |
1208 \hspace*{0pt}\\ |
1208 \hspace*{0pt}\\ |
1209 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\ |
1209 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\ |
1210 \hspace*{0pt}\\ |
1210 \hspace*{0pt}\\ |
1211 \hspace*{0pt}fun nat{\char95}aux i n =\\ |
1211 \hspace*{0pt}fun nat{\char95}aux i n =\\ |
1212 \hspace*{0pt} ~(if IntInf.<= (i, (0 :~IntInf.int)) then n\\ |
1212 \hspace*{0pt} ~(if IntInf.<= (i,~(0 :~IntInf.int)) then n\\ |
1213 \hspace*{0pt} ~~~else nat{\char95}aux (IntInf.- (i, (1 :~IntInf.int))) (Suc n));\\ |
1213 \hspace*{0pt} ~~~else nat{\char95}aux (IntInf.- (i,~(1 :~IntInf.int))) (Suc n));\\ |
1214 \hspace*{0pt}\\ |
1214 \hspace*{0pt}\\ |
1215 \hspace*{0pt}fun nat i = nat{\char95}aux i Zero{\char95}nat;\\ |
1215 \hspace*{0pt}fun nat i = nat{\char95}aux i Zero{\char95}nat;\\ |
1216 \hspace*{0pt}\\ |
1216 \hspace*{0pt}\\ |
1217 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\ |
1217 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\ |
1218 \hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\ |
1218 \hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\ |
1219 \hspace*{0pt}\\ |
1219 \hspace*{0pt}\\ |
1220 \hspace*{0pt}type 'a monoidl =\\ |
1220 \hspace*{0pt}type 'a monoidl =\\ |
1221 \hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl :~'a semigroup, neutral :~'a{\char125};\\ |
1221 \hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\ |
1222 \hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}Classes{\char95}{\char95}semigroup{\char95}monoidl A{\char95};\\ |
1222 \hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}Classes{\char95}{\char95}semigroup{\char95}monoidl A{\char95};\\ |
1223 \hspace*{0pt}fun neutral (A{\char95}:'a monoidl) = {\char35}neutral A{\char95};\\ |
1223 \hspace*{0pt}fun neutral (A{\char95}:'a monoidl) = {\char35}neutral A{\char95};\\ |
1224 \hspace*{0pt}\\ |
1224 \hspace*{0pt}\\ |
1225 \hspace*{0pt}type 'a monoid = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid :~'a monoidl{\char125};\\ |
1225 \hspace*{0pt}type 'a monoid = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid :~'a monoidl{\char125};\\ |
1226 \hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}Classes{\char95}{\char95}monoidl{\char95}monoid A{\char95};\\ |
1226 \hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}Classes{\char95}{\char95}monoidl{\char95}monoid A{\char95};\\ |
1227 \hspace*{0pt}\\ |
1227 \hspace*{0pt}\\ |
1228 \hspace*{0pt}type 'a group = {\char123}Classes{\char95}{\char95}monoid{\char95}group :~'a monoid, inverse :~'a -> 'a{\char125};\\ |
1228 \hspace*{0pt}type 'a group = {\char123}Classes{\char95}{\char95}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\ |
1229 \hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}Classes{\char95}{\char95}monoid{\char95}group A{\char95};\\ |
1229 \hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}Classes{\char95}{\char95}monoid{\char95}group A{\char95};\\ |
1230 \hspace*{0pt}fun inverse (A{\char95}:'a group) = {\char35}inverse A{\char95};\\ |
1230 \hspace*{0pt}fun inverse (A{\char95}:'a group) = {\char35}inverse A{\char95};\\ |
1231 \hspace*{0pt}\\ |
1231 \hspace*{0pt}\\ |
1232 \hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\ |
1232 \hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\ |
1233 \hspace*{0pt}\\ |
1233 \hspace*{0pt}\\ |
1234 \hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\ |
1234 \hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\ |
1235 \hspace*{0pt}\\ |
1235 \hspace*{0pt}\\ |
1236 \hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i, j);\\ |
1236 \hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\ |
1237 \hspace*{0pt}\\ |
1237 \hspace*{0pt}\\ |
1238 \hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\ |
1238 \hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\ |
1239 \hspace*{0pt}\\ |
1239 \hspace*{0pt}\\ |
1240 \hspace*{0pt}val monoidl{\char95}int =\\ |
1240 \hspace*{0pt}val monoidl{\char95}int =\\ |
1241 \hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl = semigroup{\char95}int, neutral = neutral{\char95}int{\char125}~:\\ |
1241 \hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\ |
1242 \hspace*{0pt} ~IntInf.int monoidl;\\ |
1242 \hspace*{0pt} ~IntInf.int monoidl;\\ |
1243 \hspace*{0pt}\\ |
1243 \hspace*{0pt}\\ |
1244 \hspace*{0pt}val monoid{\char95}int = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:\\ |
1244 \hspace*{0pt}val monoid{\char95}int = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:\\ |
1245 \hspace*{0pt} ~IntInf.int monoid;\\ |
1245 \hspace*{0pt} ~IntInf.int monoid;\\ |
1246 \hspace*{0pt}\\ |
1246 \hspace*{0pt}\\ |
1247 \hspace*{0pt}val group{\char95}int =\\ |
1247 \hspace*{0pt}val group{\char95}int =\\ |
1248 \hspace*{0pt} ~{\char123}Classes{\char95}{\char95}monoid{\char95}group = monoid{\char95}int, inverse = inverse{\char95}int{\char125}~:\\ |
1248 \hspace*{0pt} ~{\char123}Classes{\char95}{\char95}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\ |
1249 \hspace*{0pt} ~IntInf.int group;\\ |
1249 \hspace*{0pt} ~IntInf.int group;\\ |
1250 \hspace*{0pt}\\ |
1250 \hspace*{0pt}\\ |
1251 \hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\ |
1251 \hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\ |
1252 \hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\ |
1252 \hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\ |
1253 \hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\ |
1253 \hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\ |
1254 \hspace*{0pt}\\ |
1254 \hspace*{0pt}\\ |
1255 \hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\ |
1255 \hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\ |
1256 \hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int), k)\\ |
1256 \hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\ |
1257 \hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\ |
1257 \hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\ |
1258 \hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\ |
1258 \hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\ |
1259 \hspace*{0pt}\\ |
1259 \hspace*{0pt}\\ |
1260 \hspace*{0pt}val example :~IntInf.int =\\ |
1260 \hspace*{0pt}val example :~IntInf.int =\\ |
1261 \hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\ |
1261 \hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\ |
1262 \hspace*{0pt}\\ |
1262 \hspace*{0pt}\\ |
1263 \hspace*{0pt}end; (*struct Example*)% |
1263 \hspace*{0pt}end;~(*struct Example*)% |
1264 \end{isamarkuptext}% |
1264 \end{isamarkuptext}% |
1265 \isamarkuptrue% |
1265 \isamarkuptrue% |
1266 % |
1266 % |
1267 \endisatagquote |
1267 \endisatagquote |
1268 {\isafoldquote}% |
1268 {\isafoldquote}% |