nat-decimal.c 553 B

12345678910111213141516171819
  1. // SPDX-License-Identifier: GPL-2.0 or GPL-3.0
  2. // Copyright © 2019 Ariadne Devos
  3. // Integer model: wrap-around
  4. // Proof status: auto
  5. #define X_p decimal_p
  6. #define X_num_p decimal_num_p
  7. #define X_val decimal_val
  8. #define X_num_val decimal_num_val
  9. #define X_base 10
  10. #define sHT_X_val sHT_decimal_val
  11. #define sHT_X_base 10
  12. #define sHT_X_given_X_num_p sHT_decimal_given_decimal_num_p
  13. #define sHT_X_num_p_less sHT_decimal_num_p_less
  14. #define sHT_X_num_val_less_lt sHT_decimal_num_val_less_lt
  15. #define sHT_X_to_u32 sHT_decimal_to_u32
  16. #include "nat-generic.c"