module Rel1:sig
..end
type 'a
t
val name : 'a t -> string
Name of the relation
val create : ?k:'a CamlInterface.Univ.key -> string -> 'a t
New relation, with given name and argument
val get : 'a t -> CamlInterface.Logic.T.t -> 'a option
Check whether this term is a "R(t)" with t
an object packed
with the appropriate key, and "R" the name of the given relation
val make : 'a t -> 'a -> CamlInterface.Logic.T.t
Create a term from this relation description
val apply : 'a t -> CamlInterface.Logic.T.t -> CamlInterface.Logic.T.t
apply the relation symbol to some term
val find : CamlInterface.Logic.DB.t -> 'a t -> 'a list
Iterate on all instances of the relation present in the DB
val subset : CamlInterface.Logic.DB.t ->
'a t -> 'a t -> unit
subset db r1 r2
adds to db
the axiom that r2(X) :- r1(X)
;
in other words, r1
is a subset of r2
as a relation
val from_fun : CamlInterface.Logic.DB.t -> 'a t -> ('a -> bool) -> unit
The given function decides of the given relation (if it returns true for a constant, then the relation holds for this constant)
val add_list : CamlInterface.Logic.DB.t -> 'a t -> 'a list -> unit
Add given list of axioms
val to_string : 'a t -> string
val fmt : Format.formatter -> 'a t -> unit