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