gillian » Gillian » Gil_syntax » Lemma

Module Gil_syntax.Lemma

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;
9. lemma_location : Utils.Location.t option;

}

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