Module States.MyAsrt

type 'cp t =
  1. | Emp
    (*

    Empty heap

    *)
  2. | Pure of Gillian.Gil_syntax.Expr.t
    (*

    Pure formula

    *)
  3. | Types of (Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Type.t) list
    (*

    Typing assertion

    *)
  4. | CorePred of 'cp * Gillian.Gil_syntax.Expr.t list * Gillian.Gil_syntax.Expr.t list
    (*

    Core predicate

    *)
val map_cp : (('cp1 * Gillian.Gil_syntax.Expr.t list * Gillian.Gil_syntax.Expr.t list) -> 'cp2 * Gillian.Gil_syntax.Expr.t list * Gillian.Gil_syntax.Expr.t list) -> 'cp1 t -> 'cp2 t