blob: 676657beff943792eed46d06a560ff9117487229 (
plain)
1
2
3
4
5
6
7
8
|
viewtypedef initializable (vt:viewt@ype) =
[initialized: bool] @{ initialized = bool initialized, obj = opt (vt, initialized) }
fun {vt:viewt@ype} uninitialized (v : opt(vt,false)): initializable vt
fun {vt:viewt@ype} init_exec (x : &(initializable vt)):<!wrt> void
fun {vt:viewt@ype} init_exec$fwork (v : &vt):<!wrt> void
|
