Contains works on SeqRef.
(self)
| 2089 | assert isinstance(length, ArithRef) |
| 2090 | |
| 2091 | def test_seq_contains(self): |
| 2092 | """Contains works on SeqRef.""" |
| 2093 | from lean_py.z3 import BoolRef |
| 2094 | |
| 2095 | s = Unit(IntVal(1)) |
| 2096 | t = Unit(IntVal(1)) |
| 2097 | c = Contains(s, t) |
| 2098 | assert isinstance(c, BoolRef) |
| 2099 | |
| 2100 | def test_seq_prefix_of(self): |
| 2101 | """PrefixOf works on SeqRef.""" |