Module Logtk_proofs.LLProof

Low Level Proofs

val section : Logtk.Util.Section.t
type term = Logtk.TypedSTerm.t
type ty = term
type form = term
type inst = term list

Instantiate some binder with the following terms. Order matters.

type tag = Logtk.Proof.tag

Instantiate some binder with the following terms. Order matters.

type name = string
type t
type step =
| Goal
| Assert
| Negated_goal of t
| Trivial
| By_def of Logtk.ID.t
| Define of Logtk.ID.t
| Instantiate of {
form : t;
inst : inst;
tags : tag list;
}
| Esa of name * t list
| Inference of {
intros : term list;
local_intros : term list;
name : name;
parents : parent list;
tags : tag list;
}
type parent = {
p_proof : t;
p_inst : inst;
}
val id : t -> int
val concl : t -> form
val step : t -> step
val parents : t -> parent list
val premises : t -> t list
val p_of : t -> parent
val p_inst : t -> inst -> parent
val pp_step : step CCFormat.printer
val pp_parent : parent CCFormat.printer
val pp_id : t CCFormat.printer
val pp_res : t CCFormat.printer
val pp : t CCFormat.printer

Print only this step

val pp_dag : t CCFormat.printer

Print the whole DAG

val pp_inst : inst CCFormat.printer
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val goal : form -> t
val negated_goal : form -> t -> t
val assert_ : form -> t
val trivial : form -> t
val by_def : Logtk.ID.t -> form -> t
val define : Logtk.ID.t -> form -> t
val instantiate : ?⁠tags:tag list -> form -> t -> inst -> t
val esa : form -> name -> t list -> t
val inference : intros:term list -> local_intros:term list -> tags:tag list -> form -> name -> parent list -> t

Checking steps

type check_res =
| R_ok
| R_fail
| R_skip
val get_check_res : t -> check_res option
val set_check_res : t -> check_res -> unit
val pp_check_res : check_res CCFormat.printer

Printing

module Tbl : CCHashtbl.S with type Tbl.key = t
module Dot : sig ... end