Module Gil_syntax.LCmd

GIL Logical Commands

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

    If-then-else

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

    Branching on a FO formual

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

    Macros

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

    Assert

    *)
  5. | Assume of Formula.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 : (t -> t) option -> (Expr.t -> Expr.t) option -> (Formula.t -> Formula.t) option -> (SLCmd.t -> SLCmd.t) option -> t -> t
val pp : t Fmt.t

Pretty-printer