mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 05:41:23 +00:00
Code Activity

Fix typo in ForAll Doc

Browse source
This commit is contained in:
Saurabh Chaturvedi 2019-06-15 05:02:37 +05:30 • committed by GitHub
parent d1719ee605
commit 2fd579bdd2
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/python/z3/z3.py
View file

@ -2027,7 +2027,7 @@ def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[],
def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
"""Create a Z3 forall formula. """Create a Z3 forall formula.
The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations.
>>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x') >>> x = Int('x')