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
module E = LogtkIndex.BasicEquationModule that describes indexed equations
type rhs = E.rhsRight hand side of equation
val empty : unit -> tval is_empty : t -> boolval add_seq : t -> E.t Sequence.t -> tval remove_seq : t -> E.t Sequence.t -> tval size : t -> intNumber of indexed (in)equations
val iter : t -> (LogtkIndex.term -> E.t -> unit) -> unitIterate on indexed equations
val retrieve :
?allow_open:bool ->
?subst:LogtkIndex.subst ->
sign:bool ->
t ->
LogtkIndex.scope ->
LogtkIndex.term ->
LogtkIndex.scope ->
'a ->
('a -> LogtkIndex.term -> rhs -> E.t -> LogtkIndex.subst -> 'a) ->
'aretrieve ~sign (idx,si) (t,st) acc folds on (in)equations l ?= r of given sign and substitutions subst, such that subst(l, si) = t. It therefore finds generalizations of the query term.