package logtk
-
logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type rule = LogtkFOTerm.t * LogtkFOTerm.trewrite rule, from left to right
val empty : unit -> tval add_seq : t -> rule Sequence.t -> tval to_seq : t -> rule Sequence.tval of_seq : rule Sequence.t -> tval size : t -> intval rule_to_form : rule -> LogtkFormula.FO.tMake a formula out of a rule (an equality)
val rewrite_collect : t -> LogtkFOTerm.t -> LogtkFOTerm.t * rule listCompute normal form of the term, and also return the list of rules that were used.
val rewrite : t -> LogtkFOTerm.t -> LogtkFOTerm.tCompute normal form of the term. See rewrite_collect.