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)

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct