I_Cons (transformers.States.PMap.MakeOpen.I

Parameters

module S : MyMonadicSMemory.S

type entry = S.t

type t

val to_yojson : t -> Yojson.Safe.t

val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or

val mode : index_mode

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

val default_instantiation : Gillian.Gil_syntax.Expr.t list

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

val get : 
  t ->
  Gillian.Gil_syntax.Expr.t ->
  (Gillian.Gil_syntax.Expr.t * entry) option Gillian.Monadic.Delayed.t

val set : 
  idx:Gillian.Gil_syntax.Expr.t ->
  idx':Gillian.Gil_syntax.Expr.t ->
  entry ->
  t ->
  t

val empty : t

val fold : (Gillian.Gil_syntax.Expr.t -> entry -> 'a -> 'a) -> t -> 'a -> 'a

val for_all : (entry -> bool) -> t -> bool

val compose : t -> t -> t Gillian.Monadic.Delayed.t

val substitution_in_place : 
  Gillian.Symbolic.Subst.t ->
  t ->
  t Gillian.Monadic.Delayed.t