Module Jsil_syntax.Lemma

type lemma_spec = {
  1. pre : Asrt.t;
  2. posts : Asrt.t list;
}
type t = {
  1. name : string;
  2. params : string list;
  3. pre : Asrt.t;
  4. posts : Asrt.t list;
  5. proof : LCmd.t list option;
  6. variant : Expr.t option;
  7. existentials : string list;
}
val init_tbl : unit -> (string, t) Stdlib.Hashtbl.t
val pp : Stdlib.Format.formatter -> t -> unit