Module Rewrite.Rule

type t = rule
val of_term : Term.Rule.t -> t
val of_lit : Lit.Rule.t -> t
val proof : t -> proof
val pp : t CCFormat.printer
val as_proof : t -> Proof.t
val lit_as_proof_parent_subst : Subst.Renaming.t -> Subst.t -> Lit.Rule.t Scoped.t -> Proof.parent

Helper for clause rewriting

val set_as_proof_parents : Term.Rule_inst_set.t -> Proof.parent list

Proof parents from a set of rules instances

val make_lit : proof:Proof.t -> Literal.t -> Literal.t list list -> t

Make a literal rule