Module `Proof.Step`

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

A single step can be used to deduce several results.

type t = step

val kind : t -> kind
val parents : t -> parent list
val infos : t -> infos
val compare : t -> t -> int
val hash : t -> int
val equal : t -> t -> bool
val src : t -> source option
val trivial : t
val by_def : ID.t -> t
val define : ID.t -> source -> parent list -> t
val define_internal : ID.t -> parent list -> t
val lemma : source -> t
val intro : source -> role -> t
val assert_ : source -> t
val assert' : ?⁠loc:Loc.t -> file:string -> name:string -> unit -> t
val goal : source -> t
val goal' : ?⁠loc:Loc.t -> file:string -> name:string -> unit -> t
val inference : ?⁠infos:infos -> ?⁠tags:tag list -> rule:rule -> parent list -> t
val simp : ?⁠infos:infos -> ?⁠tags:tag list -> rule:rule -> parent list -> t
val esa : ?⁠infos:infos -> rule:rule -> parent list -> t
val to_attrs : t -> UntypedAST.attrs
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 -> 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