more correct SML for SML/NJ
authorhaftmann
Mon, 27 Jan 2025 07:39:49 +0100
changeset 81985 e23bd621eddb
parent 81984 6c052e21664f
child 81986 3863850f4b0e
more correct SML for SML/NJ
src/HOL/Library/Code_Target_Bit_Shifts.thy
--- 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;