author | haftmann |
Mon, 27 Jan 2025 07:39:49 +0100 | |
changeset 81985 | e23bd621eddb |
parent 81984 | 6c052e21664f |
child 81986 | 3863850f4b0e |
--- a/src/HOL/Library/Code_Target_Bit_Shifts.thy Mon Jan 27 07:39:48 2025 +0100 +++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy Mon Jan 27 07:39:49 2025 +0100 @@ -51,7 +51,11 @@ fun fold _ [] y = y | fold f (x :: xs) y = fold f xs (f x y); -fun replicate n x = (if n <= 0 then [] else x :: replicate (n - 1) x); +fun positive n = IntInf.> (n, 0); + +fun decr n = IntInf.- (n, 1); + +fun replicate n x = (if positive n then x :: replicate (decr n) x else []); val exp = curry IntInf.pow 2;