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 Iter.t
val all_rules : Rule.t Iter.t