Encode package:Agda
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.
Encode a mantissa and an exponent as a Double.