module name of the encoding

List of declarations

If safe, the encoding needs type checking. Type checking is done before encoding.

Signature of the encoding. Redudant with entries

encode_term sg ctx t encodes a term t. sg and ctx are used only if safe is true

decode_term t decodes a term t

encode_rule sg r encodes a rule r. sg is used only if safe is true