Rewriting is a (relatively) efficient way of computing on terms and literals using rules that come from the input. Each rule is a pair lhs, rhs (left-hand side, right-hand side) that means that objects matching lhs should be rewritten into rhs.
For term rules, lhs and rhs are both terms (with vars rhs ⊆ vars lhs).
For literal rules, lhs is an atomic literal, and rhs is a list of clauses.
This is used for Deduction Modulo in the prover.
type term = Term.ttype proof = Proof.stepval section : Util.Section.tmodule Term : sig ... endmodule Lit : sig ... endmodule Rule : sig ... endtype rule_set = Rule_set.tA constant that is defined by at least one rewrite rule
module Defined_cst : sig ... endval as_defined_cst : ID.t -> defined_cst optionval is_defined_cst : ID.t -> boolval all_cst : Defined_cst.t Iter.t