sig
type t = Proof.step
val kind : Proof.Step.t -> Proof.kind
val parents : Proof.Step.t -> Proof.parent list
val compare : Proof.Step.t -> Proof.Step.t -> int
val hash : Proof.Step.t -> int
val equal : Proof.Step.t -> Proof.Step.t -> bool
val trivial : Proof.Step.t
val by_def : Logtk.ID.t -> Proof.Step.t
val data :
Proof.statement_src -> Logtk.Type.t Logtk.Statement.data -> Proof.Step.t
val assert_ : Proof.statement_src -> Proof.Step.t
val goal : Proof.statement_src -> Proof.Step.t
val lemma : Proof.Step.t
val assert' :
?loc:Loc.t -> file:string -> name:string -> unit -> Proof.Step.t
val goal' :
?loc:Loc.t -> file:string -> name:string -> unit -> Proof.Step.t
val inference :
?check:Proof.check ->
?comment:string -> rule:Proof.rule -> Proof.parent list -> Proof.Step.t
val simp :
?check:Proof.check ->
?comment:string -> rule:Proof.rule -> Proof.parent list -> Proof.Step.t
val esa :
?check:Proof.check ->
?comment:string -> rule:Proof.rule -> Proof.parent list -> Proof.Step.t
val is_trivial : Proof.Step.t -> bool
val is_by_def : Proof.Step.t -> bool
val is_assert : Proof.Step.t -> bool
val is_goal : Proof.Step.t -> bool
val rule : Proof.Step.t -> Proof.rule option
val distance_to_goal : Proof.Step.t -> int option
val pp : Proof.Step.t CCFormat.printer
end