Imprecise error for record with invariant
The following code fails because I added an invariant {true}
to type ref
. And the error message is not helpful: Not a record field: contents
module Ref
use int.Int
type ref = { mutable contents : int}
invariant {true}
function (!) (x: ref) : int = x.contents
let ref (v: int) ensures { result = {contents = v} } = { contents = v }
end
I think the error message should be improved.