mirror of
https://github.com/Z3Prover/z3
synced 2025-06-03 04:41:21 +00:00
update documentation help to be inline with fpLT. Issue #465
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
1c630ccc9a
commit
c6c84dd59a
1 changed files with 2 additions and 2 deletions
|
@ -8829,8 +8829,8 @@ def fpLT(a, b, ctx=None):
|
||||||
>>> x, y = FPs('x y', FPSort(8, 24))
|
>>> x, y = FPs('x y', FPSort(8, 24))
|
||||||
>>> fpLT(x, y)
|
>>> fpLT(x, y)
|
||||||
x < y
|
x < y
|
||||||
>>> (x <= y).sexpr()
|
>>> (x < y).sexpr()
|
||||||
'(fp.leq x y)'
|
'(fp.lt x y)'
|
||||||
"""
|
"""
|
||||||
return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
|
return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue