with Ada.Numerics.Discrete_Random;
package body Bingo_Basket.Random with SPARK_Mode => Off is
package Random_Bingo is new Ada.Numerics.Discrete_Random
(Result_Subtype => Callable_Number);
-- The following object holds the state of a random Bingo number generator
Bingo_Gen : Random_Bingo.Generator;
function Random_Number return Callable_Number is
begin
return Random_Bingo.Random (Gen => Bingo_Gen);
end Random_Number;
begin
-- Initialize the random number generator from the system clock
Random_Bingo.Reset (Gen => Bingo_Gen);
end Bingo_Basket.Random;