Module Logtk.Rewrite

Rewriting on Terms and Literals

type term = Term.t
type defined_cst

Payload of a defined function symbol or type

type proof = Proof.step
val section : Util.Section.t
module Term : sig ... end

Rewriting on Literals and Clauses

module Lit : sig ... end

Rules in General

type rule =
| T_rule of Term.rule
| L_rule of Lit.rule
module Rule : sig ... end
module Rule_set : CCSet.S with type Rule_set.elt = rule
type rule_set = Rule_set.t

Defined Constant

A constant that is defined by at least one rewrite rule

module Defined_cst : sig ... end
val as_defined_cst : ID.t -> defined_cst option
val is_defined_cst : ID.t -> bool
val all_cst : Defined_cst.t Sequence.t
val all_rules : Rule.t Sequence.t