Open echu opened 11 years ago
Actually, this behavior should be removed. The only concatenation that will be allowed is in "norm".
norm([x; y]) gets rewritten as as norm(s,t), norm(x) <= s, and norm(y) <= t. This should be sufficient.
norm([x; y])
norm(s,t)
norm(x) <= s
norm(y) <= t
Actually, this behavior should be removed. The only concatenation that will be allowed is in "norm".
norm([x; y])
gets rewritten as asnorm(s,t)
,norm(x) <= s
, andnorm(y) <= t
. This should be sufficient.