Length works on SeqRef.
(self)
| 2081 | assert isinstance(s3, SeqRef) |
| 2082 | |
| 2083 | def test_seq_length(self): |
| 2084 | """Length works on SeqRef.""" |
| 2085 | from lean_py.z3.core import ArithRef |
| 2086 | |
| 2087 | s = Unit(IntVal(42)) |
| 2088 | length = Length(s) |
| 2089 | assert isinstance(length, ArithRef) |
| 2090 | |
| 2091 | def test_seq_contains(self): |
| 2092 | """Contains works on SeqRef.""" |