SLCmd (gillian.Gil_syntax.SLCmd)

type t =

| Fold of string * Gillian.Gil_syntax.Expr.t list * (string * (string * Gillian.Gil_syntax.Expr.t) list) option
(*
Fold predicate
*)
| Unfold of string * Gillian.Gil_syntax.Expr.t list * (string * string) list option * bool
(*
Unfold predicate
*)
| Package of {
1. lhs : string * Gillian.Gil_syntax.Expr.t list;
2. rhs : string * Gillian.Gil_syntax.Expr.t list;
}
(*
Magic wand packaging
*)
| GUnfold of string
(*
Global Unfold
*)
| ApplyLem of string * Gillian.Gil_syntax.Expr.t list * string list
(*
Apply lemma
*)
| SepAssert of Gillian.Gil_syntax.Asrt.t * string list
(*
Assert
*)
| Invariant of Gillian.Gil_syntax.Asrt.t * string list
(*
Invariant
*)
| Consume of Gillian.Gil_syntax.Asrt.t * string list
| Produce of Gillian.Gil_syntax.Asrt.t
| SymbExec

val map : 
  (t -> t) option ->
  (Gillian.Gil_syntax.Asrt.t -> Gillian.Gil_syntax.Asrt.t) option ->
  (Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t) option ->
  t ->
  t

deprecated
Use Visitors.endo instead

val pp_folding_info : 
  (string * (string * Gillian.Gil_syntax.Expr.t) list) option Fmt.t

Pretty-printer of folding info

val pp_unfold_info : (string * string) list option Fmt.t

val pp : Stdlib.Format.formatter -> t -> unit

Pretty-printer