gillian » Gillian » Gil_syntax » LCmd

Module Gil_syntax.LCmd

type t =

1. | If of Expr.t * t list * t list
   (*

   If-then-else

   *)
2. | Branch of Expr.t
   (*

   Branching on a FO formual

   *)
3. | Macro of string * Expr.t list
   (*

   Macros

   *)
4. | Assert of Expr.t
   (*

   Assert

   *)
5. | Assume of Expr.t
   (*

   Assume

   *)
6. | AssumeType of Expr.t * Type.t
   (*

   Assume Type

   *)
7. | FreshSVar of string
   (*

   x := fresh_svar()

   *)
8. | SL of SLCmd.t
   (*

   Separation-logic command

   *)

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

• deprecated

  Use Visitors.endo instead

val pp : t Fmt.t

Pretty-printer