sync

src/api/python/cvc5.pxi

@@ -573,7 +573,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 Solver solver
     def __cinit__(self, Solver solver):
@@ -597,10 +606,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.