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