Module Rewrite.Lit

type rule
module Rule : sig ... end
val normalize_clause : Literals.t -> (Literals.t list * rule * Subst.t * Scoped.scope * Subst.Renaming.t * Proof.tag list) option

normalize literals of the clause w.r.t. rules, or return None if no rule applies. The input clause lives in scope 0.

val narrow_lit : ?⁠subst:Unif_subst.t -> scope_rules:Scoped.scope -> Literal.t Scoped.t -> (rule * Unif_subst.t * Proof.tag list) Iter.t

narrow_term rules lit finds the set of rules (l --> clauses) in rules and substitutions sigma such that sigma(l) = sigma(lit)

parameter scope_rules

used for rules (LEFT)