Previous  Up  Next

Module Proof.Step

module Step: sig .. end
An inference step is composed of a set of premises, a rule, a status (theorem/trivial/equisatisfiable…), and is used to deduce new Proof.result using these premises and metadata.

A single step can be used to deduce several results.

type t = Proof.step 
val kind : t -> Proof.kind
val parents : t -> Proof.parent list
val infos : t -> Proof.infos
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 : ?infos:Proof.infos ->
       ?check:Proof.check -> rule:Proof.rule -> Proof.parent list -> t
val simp : ?infos:Proof.infos ->
       ?check:Proof.check -> rule:Proof.rule -> Proof.parent list -> t
val esa : ?infos:Proof.infos ->
       ?check:Proof.check -> rule:Proof.rule -> Proof.parent list -> t
val is_trivial : t -> bool
val is_by_def : t -> bool
val is_assert : t -> bool
Proof: the statement was asserted in some file
val is_goal : t -> bool
The statement comes from the negation of a goal in some file
val rule : t -> Proof.rule option
Rule name for Esa/Simplification/Inference steps
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