equal
deleted
inserted
replaced
432 |
432 |
433 subsection{*Floor and Ceiling Functions from the Reals to the Integers*} |
433 subsection{*Floor and Ceiling Functions from the Reals to the Integers*} |
434 |
434 |
435 definition |
435 definition |
436 floor :: "real => int" where |
436 floor :: "real => int" where |
437 "floor r = (LEAST n::int. r < real (n+1))" |
437 [code func del]: "floor r = (LEAST n::int. r < real (n+1))" |
438 |
438 |
439 definition |
439 definition |
440 ceiling :: "real => int" where |
440 ceiling :: "real => int" where |
441 "ceiling r = - floor (- r)" |
441 "ceiling r = - floor (- r)" |
442 |
442 |