From call today: can we add some syntax like pack {x=e;y=f} as r, that elaborates to something like let r = {x=e; y=f}; rewrite each e as r.x; rewrite f as r.y; to comfortably use records? Or would it be enough to define a packing function for each given type? The latter alternative would not do any rewrite in the frame.
From call today: can we add some syntax like
pack {x=e;y=f} as r, that elaborates to something likelet r = {x=e; y=f}; rewrite each e as r.x; rewrite f as r.y;to comfortably use records? Or would it be enough to define a packing function for each given type? The latter alternative would not do any rewrite in the frame.