Hi,
It seems to me that Why3 considers any record type with an invariant as
immutable. Indeed,
the following code gets me an error:
```
type lit = { var : int ; sign : bool } invariant { self.var >= 0 }
let f (ls : list lit) =
requires { forall l:lit. mem l ls } ()
```
Error: Cannot update values of type (list21 (lit19 <>)).
The problem disappears if I remove the invariant of `lit`. Is this a bug or
a feature ? Is there a way I can specify type invariants for immutable
records.
Best,
Jonathan Laurent
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
