cryptol/tests/issues/issue1093.icry

mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-03 21:37:52 +03:00
:set prover=z3
:prove \(xs:[12][0]) -> reverse (reverse xs) == xs
:prove \(xs:[0]) (ys:[0]) -> xs == ys
:prove \(xs:[0]) (ys:[0]) (zs:[0]) -> (xs # ys) # zs == xs # (ys # zs)
Add regression test for issues #1093 and #1094. 2021-03-02 23:21:53 +03:00			`:set prover=z3`
			`:prove \(xs:[12][0]) -> reverse (reverse xs) == xs`
			`:prove \(xs:[0]) (ys:[0]) -> xs == ys`
			`:prove \(xs:[0]) (ys:[0]) (zs:[0]) -> (xs # ys) # zs == xs # (ys # zs)`