# HG changeset patch # User wenzelm # Date 1464787049 -7200 # Node ID 13b67739af09cbc33922b2a81262daf2946704f7 # Parent 97b721666890a7512cec6f94e9f50410c1702268 clarified signature; diff -r 97b721666890 -r 13b67739af09 src/Pure/General/rat.ML --- a/src/Pure/General/rat.ML Wed Jun 01 15:10:27 2016 +0200 +++ b/src/Pure/General/rat.ML Wed Jun 01 15:17:29 2016 +0200 @@ -25,8 +25,8 @@ val mult: rat -> rat -> rat val neg: rat -> rat val inv: rat -> rat - val round_down: rat -> rat - val round_up: rat -> rat + val floor: rat -> int + val ceil: rat -> int end; structure Rat : RAT = @@ -91,12 +91,12 @@ | EQUAL => raise DIVZERO | GREATER => Rat (q, p)); -fun round_down (Rat (p, q)) = Rat (p div q, 1); +fun floor (Rat (p, q)) = p div q; -fun round_up (Rat (p, q)) = +fun ceil (Rat (p, q)) = (case Integer.div_mod p q of - (m, 0) => Rat (m, 1) - | (m, _) => Rat (m + 1, 1)); + (m, 0) => m + | (m, _) => m); end;