package elpi

  1. Overview
  2. Docs

Declare data from the host application that is opaque (no syntax), like int but not like list or pair

type doc = string
type name = string
type 'a declaration = {
  1. name : name;
  2. doc : doc;
  3. pp : Format.formatter -> 'a -> unit;
  4. compare : 'a -> 'a -> int;
  5. hash : 'a -> int;
  6. hconsed : bool;
  7. 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