Ref
Definitions
def fresh(rc: Region[r], x: a): Ref[a, r] \ r
SourceReturns a new reference to x
in the region rc
.
def get(rf: Ref[a, r]): a \ r
SourceReturns the element referenced by rf
.
def put(x: a, rf: Ref[a, r]): Unit \ r
SourceUpdates rf
to reference x
.
def transform(f: a -> a \ ef, rf: Ref[a, r]): Unit \ r + ef
SourceUpdates rf
to reference f
applied to the value referenced by rf
.
I.e. if rf
references x
then rf
is updated to reference f(x)
.