mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 20:18:18 +00:00
z3.py
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
666a237cbc
commit
20feecc7b0
|
@ -1625,7 +1625,7 @@ def Implies(a, b, ctx=None):
|
||||||
>>> Implies(p, q)
|
>>> Implies(p, q)
|
||||||
Implies(p, q)
|
Implies(p, q)
|
||||||
>>> simplify(Implies(p, q))
|
>>> simplify(Implies(p, q))
|
||||||
Or(Not(p), q)
|
Or(q, Not(p))
|
||||||
"""
|
"""
|
||||||
ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
|
ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
|
||||||
s = BoolSort(ctx)
|
s = BoolSort(ctx)
|
||||||
|
|
Loading…
Reference in a new issue