val remove_hidden_initializer (init: initializer_t) (mem: Armada.Memory.t) : GTot Armada.Memory.t
val remove_hidden_initializer (init: initializer_t) (mem: Armada.Memory.t) : GTot Armada.Memory.t
let remove_hidden_initializer
  (init: initializer_t)
  (mem: Armada.Memory.t)
  : GTot Armada.Memory.t =
  let root_id = RootIdGlobal init.var_id in
  Spec.Map.upd mem root_id RootInvalid
module Strategies.VarHiding.Initialization

open Armada.Base
open Armada.Init
open Armada.Memory
open Armada.Type
open Spec.List
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.GlobalVars
open Strategies.GlobalVars.Types
open Strategies.VarHiding.Defs
/
Strategies.VarHiding.Defs.fst.checked Strategies.GlobalVars.Types.fst.checked Strategies.GlobalVars.fst.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Base.fst.checked
Strategies.VarHiding.Initialization.fsti
init: Armada.Init.initializer_t -> mem: Armada.Memory.t -> Prims.GTot Armada.Memory.t
Armada.Init.initializer_t Armada.Memory.t Spec.Map.upd Armada.Base.root_id_t Armada.Memory.root_t Armada.Memory.RootInvalid Armada.Base.RootIdGlobal Armada.Init.__proj__Mkinitializer_t__item__var_id
let remove_hidden_initializer (init: initializer_t) (mem: Armada.Memory.t) : GTot Armada.Memory.t =
  
let root_id = RootIdGlobal init.var_id in
Spec.Map.upd mem root_id RootInvalid