package logtk

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

Parameters

module I (E : LogtkIndex.EQUATION) : LogtkIndex.UNIT_IDX with module E = E

Signature

type t

rewrite rule, from left to right

val empty : unit -> t
val add : t -> rule -> t
val add_seq : t -> rule Sequence.t -> t
val add_list : t -> rule list -> t
val to_seq : t -> rule Sequence.t
val of_seq : rule Sequence.t -> t
val of_list : rule list -> t
val size : t -> int
val iter : t -> (rule -> unit) -> unit
val rule_to_form : rule -> LogtkFormula.FO.t

Make a formula out of a rule (an equality)

val rewrite_collect : t -> LogtkFOTerm.t -> LogtkFOTerm.t * rule list

Compute normal form of the term, and also return the list of rules that were used.

val rewrite : t -> LogtkFOTerm.t -> LogtkFOTerm.t

Compute normal form of the term. See rewrite_collect.