String concatenation is associative.
(self, kernel)
| 800 | """Universal string properties.""" |
| 801 | |
| 802 | def test_concat_assoc(self, kernel): |
| 803 | """String concatenation is associative.""" |
| 804 | x, y, z = Strings("x y z") |
| 805 | g = Goal() |
| 806 | g.add(StrConcat(StrConcat(x, y), z) == StrConcat(x, StrConcat(y, z))) |
| 807 | assert len(Tactic("simp [String.append_assoc]").apply(g)) == 0 |
| 808 | |
| 809 | def test_empty_concat_left(self, kernel): |
| 810 | x = String("x") |