-
Andrei Paskevich authored
Type declarations for records (incuding the private records) can now be followed by a "witness": a set of values for the record fields that must satisfy the type invariant (if any). The fields must be initialized with pure terminating program expressions. The current syntax, proposed by Martin, is type t 'a = { f: ty1; g: ty2 } invariant { J[f,g] } by { f = e1; g = e2 } The generated proof obligation is the VC for let g = e2 in let f = e1 in assert { J[f,g] } In absence of an explicit witness, an existential proof obligation "exists f,g. J[f,g]" is produced.
15fc3d65