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 = stepval hash : t -> intval trivial : tval inferences_performed : t -> intval count_rules : name:string -> t -> intval has_ho_step : t -> boolval to_attrs : t -> UntypedAST.attrsval is_inference : t -> boolval is_trivial : t -> boolval is_by_def : t -> boolval is_assert : t -> boolProof: the statement was asserted in some file
val is_goal : t -> boolThe statement comes from the negation of a goal in some file
val distance_to_goal : t -> int optiondistance_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