for.hs
for as rforall a, b.
s:(Set >Int) ~>
(set:{v:Set >Int | setSubset s v} ~>
x:a ->
SetST
<{v:Set >Int | v == set}
>{v:Set >Int | setSubset set v}
>b) ->
List >a ->
SetST
<{v:Set >Int | v == s}
>{v:Set >Int | setSubset s v}
>b
-- We can implement for using Lists (see append.hs)
for = 0
f as forall a. fs:(Set >Int) ~> x:a -> SetST <{v:Set >Int | v == fs} >{v:Set >Int | setSubset fs v} >Int
f = 0
foo :: foos:(Set >Int) ~> acts:(List >Int) -> SetST <{v:Set >Int | v == foos} >{v:Set >Int | setSubset foos v} >Int
foo = \acts -> for f acts
pure as rforall a. x:a -> List >a
pure = 0
baz :: s:(Set >Int) ~> Int -> SetST <{v:Set >Int | v == s} >{v:Set >Int | setSubset s v} >Int
baz = \i -> for baz (pure i)
bar :: se:(Set >Int) ~> cur:{v:Int | v ∈ se} -> SetST <{v:Set >Int | v == se} >{v:Set >Int | setSubset se v} >Int
bar = \i -> for bar (pure i)