From 4f25886548205ce38643ad1aafe1a8c2774d7c6e Mon Sep 17 00:00:00 2001
From: Yoni Zohar <yonizohar@Yonis-MacBook-Pro.local>
Date: Tue, 6 Jun 2023 09:48:08 +0300
Subject: [PATCH 1/2] merging

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

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 17a8b30f599..03c18cbea8f 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -573,16 +573,7 @@ cdef class DatatypeSelector:
 
 
 cdef class 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`.
-    """
+    """Wrapper class for :cpp:class:`cvc5::api::Op`."""
     cdef c_Op cop
     cdef Solver solver
     def __cinit__(self, Solver solver):
@@ -606,10 +597,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.

From cd73656a5c9145770638b0512f0110916ad6face Mon Sep 17 00:00:00 2001
From: Yoni Zohar <yoni206@gmail.com>
Date: Wed, 14 Jun 2023 11:38:09 +0300
Subject: [PATCH 2/2] 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 6727d30376d..1629a8d1817 100644
--- a/src/api/python/cvc5.pxi
+++ b/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.