We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 316c0e5 commit 39620e6Copy full SHA for 39620e6
cvc5_pythonic_api/cvc5_pythonic.py
@@ -8688,14 +8688,11 @@ def CreateDatatypes(*ds):
8688
result.append(dref)
8689
return tuple(result)
8690
8691
-class DatatypeSort:
8692
- """Unresolved datatype sorts."""
8693
-
8694
- def __init__(self, name, ctx=None):
8695
- self.name = name
8696
- self.ctx = _get_ctx(ctx)
8697
- self.ast = self.ctx.tm.mkUnresolvedDatatypeSort(name)
8698
+def DatatypeSort(name, ctx=None):
+ """Create a reference to a sort that will be declared as a recursive datatype"""
+ ctx = _get_ctx(ctx)
+ s = ctx.tm.mkUnresolvedDatatypeSort(name)
+ return SortRef(s, ctx)
8699
8700
class DatatypeSortRef(SortRef):
8701
"""Datatype sorts."""
0 commit comments