From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Fri, 7 Jan 2022 04:37:08 +0000 (-0800)
Subject: Document quantifiers in idiomatic python API (#7880)
X-Git-Tag: cvc5-1.0.0~587
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a2f099d72f65bbfe4224bc96ed16c1b423774760;p=cvc5.git

Document quantifiers in idiomatic python API (#7880)
---

diff --git a/docs/api/python/z3compat/quant.rst b/docs/api/python/z3compat/quant.rst
index 8f4a756c7..ecf85445a 100644
--- a/docs/api/python/z3compat/quant.rst
+++ b/docs/api/python/z3compat/quant.rst
@@ -1,4 +1,20 @@
 Quantifiers
 ============
 
+Builders
+------------------
+.. autofunction:: cvc5_z3py_compat.ForAll
+.. autofunction:: cvc5_z3py_compat.Exists
+.. autofunction:: cvc5_z3py_compat.Lambda
+
+Testers
+-------------------
 .. autofunction:: cvc5_z3py_compat.is_var
+.. autofunction:: cvc5_z3py_compat.is_quantifier
+
+Classes
+-------
+.. autoclass:: cvc5_z3py_compat.QuantifierRef
+   :members:
+   :special-members:
+