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
LogtkFOTerm rewriting
Ordered rewriting
Although this module is parametrized by an EQUATION module, it only deals with positive equations. Negative equations will be discarded.
module type ORDERED = sig ... endmodule MakeOrdered
(E : LogtkIndex.EQUATION with type rhs = LogtkFOTerm.t) :
ORDERED with module E = ERegular rewriting
module type SIG_TRS = sig ... endmodule MakeTRS
(I :
functor (E : LogtkIndex.EQUATION) ->
LogtkIndex.UNIT_IDX with module E = E) :
SIG_TRSFOLogtkFormula rewriting
module FormRW : sig ... end