Add injectivity for type invariant
type t = {
v: int;
} invariant { 0 <= v }
It is currently not possible to prove that:
forall x1 x2:t. x1.v = x2.v -> x1 = x2
Which is compiled to:
forall x1 x2:t. (view x1).v = (view x2).v -> x1 = x2
We need to add the property that view
is injective, for example using mk
its inverse:
forall x:t [view x]. mk (view x) = x
Decision
So, we agreed that adding
t'mk
for constructing a non-private typet
from its fields is a good idea.