Module Gil_syntax.Lemma

GIL Lemmas

type spec = {
  1. lemma_hyp : Gillian.Gil_syntax.Asrt.t;
    (*

    Hypothesis

    *)
  2. lemma_concs : Gillian.Gil_syntax.Asrt.t list;
    (*

    Conclusion

    *)
  3. lemma_spec_variant : Gillian.Gil_syntax.Expr.t option;
    (*

    Variant

    *)
}
type t = {
  1. lemma_name : string;
    (*

    Name

    *)
  2. lemma_source_path : string option;
  3. lemma_internal : bool;
  4. lemma_params : string list;
    (*

    Parameters

    *)
  5. lemma_specs : spec list;
    (*

    Specs of the Lemma

    *)
  6. lemma_proof : Gillian.Gil_syntax.LCmd.t list option;
    (*

    (Optional) Proof

    *)
  7. lemma_variant : Gillian.Gil_syntax.Expr.t option;
    (*

    Variant

    *)
  8. lemma_existentials : string list;
}
val pp : Stdlib.Format.formatter -> t -> unit

Pretty-printer

val parameter_types : (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t -> t -> t

Infers types of parameters and adds them to the contained assertions

val add_param_bindings : t -> t

Adds bindings from parameters to logical variables