mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
hash update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d0fc463a0c
commit
1b910c4ed2
|
@ -1627,7 +1627,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(q, Not(p))
|
Or(Not(p), q)
|
||||||
"""
|
"""
|
||||||
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