Agda.TypeChecking.Serialise

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

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.

Decodes an uncompressed bytestring (without extra hashes or magic numbers). The result depends on the include path.

Returns Nothing if a decoding error is encountered.

Decodes an interface. The result depends on the include path.

Returns Nothing if the file does not start with the right magic number or some other decoding error is encountered.