Module Gil_syntax.LCmd

GIL Logical Commands

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
val pp : t Fmt.t

Pretty-printer