src/Pure/library.ML
changeset 69769 c19a32cb9625
parent 69468 54a95e1199cb
child 70464 2d6a489adb01
equal deleted inserted replaced
69767:d10fafeb93c0 69769:c19a32cb9625
   249 fun (f oo g) x y = f (g x y);
   249 fun (f oo g) x y = f (g x y);
   250 fun (f ooo g) x y z = f (g x y z);
   250 fun (f ooo g) x y z = f (g x y z);
   251 fun (f oooo g) x y z w = f (g x y z w);
   251 fun (f oooo g) x y z w = f (g x y z w);
   252 
   252 
   253 (*function exponentiation: f (... (f x) ...) with n applications of f*)
   253 (*function exponentiation: f (... (f x) ...) with n applications of f*)
   254 fun funpow (0 : int) _ = I
   254 fun funpow (0: int) _ x = x
   255   | funpow n f = f #> funpow (n - 1) f;
   255   | funpow n f x = funpow (n - 1) f (f x);
   256 
   256 
   257 fun funpow_yield (0 : int) _ x = ([], x)
   257 fun funpow_yield (0 : int) _ x = ([], x)
   258   | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
   258   | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
   259 
   259 
   260 
   260