package BigNumPkg.Even is

   --  Type Even_BigNum shares implementation with BigNum,
   --    but it is distinct from type BigNum.
   --  Type Even_BigNum inherits all BigNum procedures and functions.
   --  In the inherited routinesll parameters are implicitly changed
   --    from BigNum to Even_BigNum.
   type Even_BigNum is new BigNum with
      Dynamic_Predicate => is_even(BigNum(Even_BigNum));

   --  Returns true if b is even, false otherwise
   function is_even (b : BigNum) return Boolean;

   --  Returns next larger or smaller bignum, depending on value of toward.
   --  If toward is larger, next larger bignum is returned.
   --  If toward is smaller, next smaller bignum is returned.
   --    (This is similar to Float'Adjacent which returns the next float
   --  Since b is odd, the returned value will be even
   function make_even (b : BigNum; toward : BigNum)  return Even_BigNum
      with pre => not is_even(b);

end BigNumPkg.Even;