Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Serialise
Description
Structure-sharing serialisation of Agda interface files.
Synopsis
encode :: EmbPrj a => a -> TCM ByteString
encodeFile :: EmbPrj a => FilePath -> a -> TCM ()
decode :: EmbPrj a => ByteString -> TCM (Maybe a)
decodeFile :: EmbPrj a => FilePath -> TCM (Maybe a)
class Typeable a => EmbPrj a
Documentation
encode :: EmbPrj a => a -> TCM ByteStringSource
Encodes something. To ensure relocatability file paths in positions are replaced with module names.
encodeFileSource
:: EmbPrj a
=> FilePathThe encoded data is written to this file.
-> aSomething.
-> TCM ()
Encodes something. To ensure relocatability file paths in positions are replaced with module names.
decode :: EmbPrj a => ByteString -> TCM (Maybe a)Source

Decodes something. The result depends on the include path.

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

decodeFile :: EmbPrj a => FilePath -> TCM (Maybe a)Source

Decodes something. 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.

class Typeable a => EmbPrj a Source
Produced by Haddock version 2.6.1