Lambda sort and DatatypeRef in _to_expr_ref #100

def Const(name, sort):
    # _to_expr doesn't have a DatatypeRef case
    x = cvc5.pythonic.Const(name, sort)
    if isinstance(sort, DatatypeSortRef):
        x = DatatypeRef(x.ast, x.ctx, x.reverse_children)
    return x

def _qsort(self):
    if self.is_lambda():
        return ArraySort(self.var_sort(0), self.body().sort())
    else:
        return BoolSort(self.ctx)


QuantifierRef.sort = _qsort

________________________________________________________________ ERROR collecting tests/test_kernel.py ________________________________________________________________
tests/test_kernel.py:9: in <module>
    import knuckledragger.theories.Interval
knuckledragger/theories/Interval.py:9: in <module>
    setof = kd.define("setof", [i], smt.Lambda([x], smt.And(i.lo <= x, x <= i.hi)))
knuckledragger/kernel.py:132: in define
    f(*args) == body
../../../.local/lib/python3.10/site-packages/cvc5/pythonic/cvc5_pythonic.py:375: in __eq__
    return BoolRef(c.solver.mkTerm(Kind.EQUAL, a.as_ast(), b.as_ast()), c)
cvc5.pxi:2556: in cvc5.cvc5_python_base.Solver.mkTerm
    ???
cvc5.pxi:1538: in cvc5.cvc5_python_base.TermManager.mkTerm
    ???
E   RuntimeError: Subexpressions must have the same type:
E   Equation: (= (setof i) (lambda ((x Real)) (and (<= (lo i) x) (<= x (hi i)))))
E   Type 1: (Array Real Bool)
E   Type 2: (-> Real Bool)