← Back to branch summary

~rosivaldo-fa/set-theory/incremental

« back to all changes in this revision

Viewing changes to src/st_tests/properties/numbers_properties/rational_number_properties.e

  • Committer: rosivaldo.fa
  • Date: 2022-01-13 18:38:21 UTC
  • Revision ID: rosivaldo.fa@gmail.com-20220113183821-pcyywdq2g8rogcf1
{STI_RATIONAL_NUMBER}.is_integer

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/st_tests/properties/numbers_properties/rational_number_properties.e
37
37
                        is_negative_infinity_ok as real_is_negative_infinity_ok,
38
38
                        is_positive_infinity_ok as real_is_positive_infinity_ok,
39
39
                        is_infinite_ok as real_is_infinite_ok,
40
 
--                      is_integer_ok as real_is_integer_ok,
 
40
                        is_integer_ok as real_is_integer_ok,
41
41
                        equals_ok as real_equals_ok,
42
42
                        expanded_equals_ok as complex_expanded_equals_ok,
43
43
                        expanded_unequals_ok as complex_expanded_unequals_ok,
90
90
                                neutral_right_term: (pq + pq_0) ≍ pq
91
91
                                quasi_neutral_minuend: (pq_0 - pq) ≍ - pq
92
92
                                neutral_subtrahend: (pq - pq_0) ≍ pq
 
93
 
 
94
                                        pq_0_multipliable_pq: pq_0.multipliable (pq) -- pq_0.q = 1
93
95
                                absorbing_left_factor: (pq_0 ⋅ pq) ≍ pq_0
 
96
 
 
97
                                        pq_multipliable_pq_0: pq.multipliable (pq_0) -- pq_0.q = 1
94
98
                                absorbing_right_factor: (pq ⋅ pq_0) ≍ pq_0
95
 
                                absorbing_dividend: pq_0.divisible (pq) implies
96
 
                                        (pq_0 / pq) ≍ pq_0
 
99
 
 
100
                                absorbing_dividend: pq_0.divisible (pq) implies (pq_0 / pq) ≍ pq_0
97
101
                                negative_exponent: -- TODO: Take a real exponent instead.
98
102
                                        pq < Zero implies (pq_0 ^ pq).is_positive_infinity
99
103
                                to_power_zero: (pq_0 ^ Zero) ≍ one
258
262
                end
259
263
 
260
264
note
261
 
        copyright: "Copyright (c) 2012-2021, Rosivaldo Fernandes Alves"
 
265
        copyright: "Copyright (c) 2012-2022, Rosivaldo Fernandes Alves"
262
266
        license: "[
263
267
                Eiffel Forum License v2
264
268
                (see http://www.eiffel.com/licensing/forum.txt)