package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

Rewriting on Terms

type rule
module Rule : sig ... end
module Set : sig ... end
type rule_set = Set.t
module Rule_inst_set : sig ... end

Set of rules with their instantiation

val normalize_term : ?max_steps:int -> term -> term * Rule_inst_set.t

normalize t computes the normal form of t w.r.t the set of rewrite rules stored in IDs. Returns the new term and the set of rules that were used

  • parameter max_steps

    number of steps after which we stop

val normalize_term_fst : ?max_steps:int -> term -> term

Same as normalize_term but ignores the set of rules

val narrow_term : ?subst:Unif_subst.t -> scope_rules:Scoped.scope -> term Scoped.t -> (rule * Unif_subst.t) Iter.t

narrow_term ~scope_rule t finds the set of rules (l --> r) in IDs and substitutions sigma such that sigma(l) = sigma(t)

  • parameter scope_rules

    used for rules (LEFT)