diff options
| author | Avi Shinnar | 2020-12-05 21:56:15 -0500 |
|---|---|---|
| committer | Avi Shinnar | 2020-12-09 08:40:11 -0500 |
| commit | 29d2ffb5f5569efe8614efa30be560efc72a34f5 (patch) | |
| tree | 64d49df94da5c5b2d4d5674d7caacf7b36c29822 /kernel/nativevalues.mli | |
| parent | 9e0ca704fa8273a8337ff9e118d2d08620af8962 (diff) | |
Redefines exp_ineq1 to hold for all non-zero numbers.
The original (which holds only for positive numbers) is now called exp_ineq1_pos.
A version that holds only for negative numbers is added as exp_ineq1_neg.
Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <).
Co-authored-by: Barry M. Trager <bmt@us.ibm.com>
Diffstat (limited to 'kernel/nativevalues.mli')
0 files changed, 0 insertions, 0 deletions