Module CLogic.CProg

type t = {
  1. preds : CPred.t list;
  2. specs : CSpec.t list;
  3. lemmas : CLemma.t list;
  4. only_specs : CSpec.t list;
  5. imports : (string * bool) list;
  6. abs_preds : CAbsPred.t list;
}
val add_only_spec : CSpec.t -> t -> t
val add_imports : (string * bool) list -> t -> t
val add_pred : CPred.t -> t -> t
val add_abs_pred : CAbsPred.t -> t -> t
val add_spec : CSpec.t -> t -> t
val add_lemma : CLemma.t -> t -> t
val merge : t -> t -> t
val empty : t
val pp : Stdlib.Format.formatter -> t -> unit