diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py
index 685dce9..ffc4da5 100644
--- a/cvc5_pythonic_api/cvc5_pythonic.py
+++ b/cvc5_pythonic_api/cvc5_pythonic.py
@@ -8689,6 +8689,13 @@ def CreateDatatypes(*ds):
     return tuple(result)
 
 
+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)
+
+
 class DatatypeSortRef(SortRef):
     """Datatype sorts."""
 
diff --git a/test/pgm_outputs/example_datatypes.py.out b/test/pgm_outputs/example_datatypes.py.out
index f5d842c..ab1962a 100644
--- a/test/pgm_outputs/example_datatypes.py.out
+++ b/test/pgm_outputs/example_datatypes.py.out
@@ -13,3 +13,6 @@ t is a 'cons': True
 
 [a = 51]
 proved
+
+Sorts match: True
+Operation on resolved sort works: True
diff --git a/test/pgms/example_datatypes.py b/test/pgms/example_datatypes.py
index fa6e06c..44c0027 100644
--- a/test/pgms/example_datatypes.py
+++ b/test/pgms/example_datatypes.py
@@ -42,3 +42,18 @@
     solve(List.head(List.cons(a, List.nil)) > 50)
 
     prove(Not(List.is_nil(List.cons(a, List.nil))))
+
+    print()
+
+    # Test DatatypeSort for unresolved datatype sorts.
+    SomeType = Datatype('SomeType')
+    SomeTypeSort = DatatypeSort('SomeType')
+    SomeType.declare('nil')
+    SomeType.declare('some', ('someof', SeqSort(SomeTypeSort), ))
+    SomeTypeSort = SomeType.create()
+
+    nil = SomeTypeSort.nil
+    some = SomeTypeSort.some(Unit(nil))
+
+    print("Sorts match:", SomeTypeSort == SomeTypeSort.someof(some)[0].sort())
+    print("Operation on resolved sort works:", simplify(SomeTypeSort.is_nil(SomeTypeSort.someof(some)[0])))