elpi

ELPI - Embeddable λProlog Interpreter
Library elpi
Module Elpi . API . OpaqueData
type doc = string
type name = string
type 'a declaration = {
name : name;
doc : doc;
pp : Format.formatter -> 'a -> unit;
compare : 'a -> 'a -> int;
hash : 'a -> int;
hconsed : bool;
constants : (name * 'a) list;
}

The eq function is used by unification. Limitation: unification of * two cdata cannot alter the constraint store. This can be lifted in the * future if there is user request. * * If the hconsed is true, then the readback function is * automatically hashcons the data using the eq and hash functions.

val declare : 'a declaration -> 'a Conversion.t