module Step:sig
..end
Proof.result
using these premises and metadata.
A single step can be used to deduce several results.
typet =
Proof.step
val kind : t -> Proof.kind
val parents : t -> Proof.parent list
val compare : t -> t -> int
val hash : t -> int
val equal : t -> t -> bool
val trivial : t
val by_def : Logtk.ID.t -> t
val data : Proof.statement_src -> Logtk.Type.t Logtk.Statement.data -> t
val assert_ : Proof.statement_src -> t
val goal : Proof.statement_src -> t
val lemma : t
val assert' : ?loc:Loc.t -> file:string -> name:string -> unit -> t
val goal' : ?loc:Loc.t -> file:string -> name:string -> unit -> t
val inference : ?check:Proof.check ->
?comment:string -> rule:Proof.rule -> Proof.parent list -> t
val simp : ?check:Proof.check ->
?comment:string -> rule:Proof.rule -> Proof.parent list -> t
val esa : ?check:Proof.check ->
?comment:string -> rule:Proof.rule -> Proof.parent list -> t
val is_trivial : t -> bool
val is_by_def : t -> bool
val is_assert : t -> bool
val is_goal : t -> bool
val rule : t -> Proof.rule option
val distance_to_goal : t -> int option
distance_to_conjecture p
returns None
if p
has no ancestor
that is a conjecture (including p
itself). It returns Some d
if d
is the distance, in the proof graph, to the closest
conjecture ancestor of p
val pp : t CCFormat.printer