Module Gil_syntax.Lemma

GIL Lemmas

type spec = {
  1. lemma_hyp : Asrt.t Utils.Location.located;
    (*

    Hypothesis

    *)
  2. lemma_concs : Asrt.t Utils.Location.located list;
    (*

    Conclusion

    *)
  3. lemma_spec_variant : 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 : LCmd.t list option;
    (*

    (Optional) Proof

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

    Variant

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

Pretty-printer

val parameter_types : (string, 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