gillian » Gillian » Gil_syntax » SLCmd

Module Gil_syntax.SLCmd

type t =

1. | Fold of string * Expr.t list * (string * (string * Expr.t) list) option
   (*

   Fold predicate

   *)
2. | Unfold of string * Expr.t list * (string * string) list option * bool
   (*

   Unfold predicate

   *)
3. | Package of{
   1. lhs : string * Expr.t list;
   2. rhs : string * Expr.t list;
   }
   (*

   Magic wand packaging

   *)
4. | GUnfold of string
   (*

   Global Unfold

   *)
5. | ApplyLem of string * Expr.t list * string list
   (*

   Apply lemma

   *)
6. | SepAssert of Asrt.t * string list
   (*

   Assert

   *)
7. | Invariant of Asrt.t * string list
   (*

   Invariant

   *)
8. | Consume of Asrt.t * string list
9. | Produce of Asrt.t
10. | SymbExec

val map : (Asrt.t -> Asrt.t) -> (Expr.t -> Expr.t) -> t -> t

• deprecated

  Use Visitors.endo instead

val pp_folding_info : (string * (string * 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