Module Sidekick_proof.Pterm

Proof terms.

A proof term is the description of a reasoning step, that yields a clause.

type step_id = Step.id
type local_ref = Step.id

A local reference is a step id that is only valid in the scope of a P_let. Typically one can use negative integers to avoid accidental shadowing.

type rule_apply = {
  1. rule_name : string;
  2. lit_args : lit list;
  3. term_args : Sidekick_core.Term.t list;
  4. subst_args : Sidekick_core.Subst.t list;
  5. premises : step_id list;
  6. indices : int list;
}
type t =
  1. | P_ref of step_id
  2. | P_local of local_ref
    (*

    Local reference, in a let

    *)
  3. | P_let of (local_ref * t) list * t
  4. | P_apply of rule_apply
type delayed = unit -> t
include Sidekick_sigs.PRINT with type t := t
val ref : step_id -> t
val local_ref : local_ref -> t
val let_ : (local_ref * t) list -> t -> t
val delay : (unit -> t) -> delayed
val dummy : t

Reference to the dummy step

val apply_rule : ?lits:lit list -> ?terms:Sidekick_core.Term.t list -> ?substs:Sidekick_core.Subst.t list -> ?premises:step_id list -> ?indices:int list -> string -> t

Serialize