Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Data of the host program that is opaque to Elpi.
type 'a data_declaration = {
data_name : string;
data_pp : Stdlib.Format.formatter -> 'a -> unit;
data_eq : 'a -> 'a -> bool;
data_hash : 'a -> int;
data_hconsed : bool;
}
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 data_hconsed is true, then the cin
function below will * automatically hashcons the data using the eq
and hash
functions.
val declare : 'a data_declaration -> 'a cdata
val pp : Stdlib.Format.formatter -> t -> unit
val show : t -> string
val hash : t -> int
val name : t -> string