Module Proof.StepSource

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.

Sourcetype t = step
Sourceval kind : t -> kind
Sourceval parents : t -> parent list
Sourceval infos : t -> infos
Sourceval compare : t -> t -> int
Sourceval hash : t -> int
Sourceval equal : t -> t -> bool
Sourceval src : t -> source option
Sourceval trivial : t
Sourceval by_def : ID.t -> t
Sourceval define : ID.t -> source -> parent list -> t
Sourceval define_internal : ID.t -> parent list -> t
Sourceval lemma : source -> t
Sourceval intro : source -> role -> t
Sourceval assert_ : source -> t
Sourceval assert' : ?loc:Loc.t -> file:string -> name:string -> unit -> t
Sourceval goal : source -> t
Sourceval goal' : ?loc:Loc.t -> file:string -> name:string -> unit -> t
Sourceval inference : ?infos:infos -> ?tags:tag list -> rule:rule -> parent list -> t
Sourceval simp : ?infos:infos -> ?tags:tag list -> rule:rule -> parent list -> t
Sourceval esa : ?infos:infos -> rule:rule -> parent list -> t
Sourceval to_attrs : t -> UntypedAST.attrs
Sourceval is_trivial : t -> bool
Sourceval is_by_def : t -> bool
Sourceval is_assert : t -> bool

Proof: the statement was asserted in some file

Sourceval is_goal : t -> bool

The statement comes from the negation of a goal in some file

Sourceval rule : t -> rule option

Rule name for Esa/Simplification/Inference steps

Sourceval 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