diff -r 3863850f4b0e -r 5dc2c98a6f16 src/HOL/Library/Code_Target_Bit_Shifts.thy --- a/src/HOL/Library/Code_Target_Bit_Shifts.thy Mon Jan 27 13:13:28 2025 +0100 +++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy Mon Jan 27 13:13:30 2025 +0100 @@ -101,7 +101,7 @@ end;; \ for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit and (Haskell) \ -module Bit_Shifts where +module Bit_Shifts (push, drop, push', drop') where import Prelude (Int, Integer, toInteger, fromInteger, maxBound, divMod, (-), (<=), abs, flip) import GHC.Bits (Bits) @@ -123,17 +123,17 @@ {- The implementations are formally total, though indices >~ maxIndex will produce heavy computation load -} -push' :: Int -> Int -> Int -push' i = flip shiftL (abs i) - push :: Integer -> Integer -> Integer push i = fold (flip shiftL) (splitIndex (abs i)) +drop :: Integer -> Integer -> Integer +drop i = fold (flip shiftR) (splitIndex (abs i)) + +push' :: Int -> Int -> Int +push' i = flip shiftL (abs i) + drop' :: Int -> Int -> Int drop' i = flip shiftR (abs i) - -drop :: Integer -> Integer -> Integer -drop i = fold (flip shiftR) (splitIndex (abs i)) \ for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit and (Scala) \ object Bit_Shifts {