From 1df0e7398556372c920295a8fe6398b6c9030dae Mon Sep 17 00:00:00 2001
From: Yoni Zohar <yoni206@gmail.com>
Date: Wed, 14 Jun 2023 11:38:09 +0300
Subject: [PATCH] sync

---
 src/api/python/cvc5.pxi | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index cd28c507ce9..ce806e57899 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -897,7 +897,16 @@ cdef class DatatypeSelector:
 # ----------------------------------------------------------------------------
 
 cdef class Op:
-    """Wrapper class for :cpp:class:`cvc5::api::Op`."""
+    """
+        A cvc5 operator.
+
+        An operator is a term that represents certain operators,
+        instantiated with its required parameters, e.g.,
+        a term of kind
+        :py:obj:`BITVECTOR_EXTRACT <Kind.BITVECTOR_EXTRACT>`.
+
+        Wrapper class for :cpp:class:`cvc5::Op`.
+    """
     cdef c_Op cop
     cdef TermManager tm
 
@@ -918,10 +927,10 @@ cdef class Op:
 
     def getKind(self):
         """
-            :return: the kind of this operator.
+            :return: The kind of this operator.
         """
-        return kind(<int> self.cop.getKind())
-    
+        return Kind(<int> self.cop.getKind())
+
     def isIndexed(self):
         """
             :return: True iff this operator is indexed.