I (transformers.States.PMap.SplitImplSat.I)

val mode : index_mode

val is_valid_index : 
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Expr.t option Gillian.Monadic.Delayed.t

val make_fresh : unit -> Gillian.Gil_syntax.Expr.t Gillian.Monadic.Delayed.t

val default_instantiation : Gillian.Gil_syntax.Expr.t list