Encode package:Agda

Efficiently serialize a JSON value as a lazy ByteString. This is implemented in terms of the ToJSON class's toEncoding method.

Encodes something. To ensure relocatability file paths in positions are replaced with module names.

The JSON version ofPrettyTCM, for encoding JSON value in TCM

Haskell module names have to satisfy the Haskell (including the hierarchical module namespace extension) lexical syntax:

modid -> [modid.] large {small | large | digit | ' }

encodeModuleName is an injective function into the set of module names defined by modid. The function preserves .s, and it also preserves module names whose first name part is not mazstr. Precondition: The input must not start or end with ., and no two .s may be adjacent.

Turns strings into valid Haskell identifiers. In order to avoid clashes with names of regular Haskell definitions (those not generated from Agda definitions), make sure that the Haskell names are always used qualified, with the exception of names from the prelude.

Efficiently serialize a JSON value as a lazy ByteString and write it to a file.

Encodes an interface. To ensure relocatability file paths in positions are replaced with module names. An uncompressed bytestring corresponding to the encoded interface is returned.

Subphase for Serialization.

Encode a mantissa and an exponent as a Double.