Add 'update' for State in ST
commit195ad13dc9db46bee590156f78563a625827294f
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 20 Mar 2017, 09:58 (10 years ago)
parentbce80e0
libs/contrib/Control/ST.idr+8
@@ -483,6 +483,14 @@ write : (lbl : Var) ->
483483 STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))
484484write lbl {prf} val = Write lbl prf (Value val)
485485
486+export
487+update : (lbl : Var) ->
488+ {auto prf : InState lbl (State ty) ctxt} ->
489+ (ty -> ty') ->
490+ STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))
491+update lbl f = do x <- read lbl
492+ write lbl (f x)
493+
486494namespace Loop
487495 export
488496 (>>=) : STrans m a st1 st2_fn ->