|
Agda.TypeChecking.Serialise |
|
|
Description |
Structure-sharing serialisation of Agda interface files.
|
|
Synopsis |
|
|
|
Documentation |
|
|
Encodes something. To ensure relocatability file paths in
positions are replaced with module names.
|
|
|
:: EmbPrj a | | => FilePath | The encoded data is written to this file.
| -> a | Something.
| -> TCM () | | Encodes something. To ensure relocatability file paths in
positions are replaced with module names.
|
|
|
|
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.
|
|
|
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.
|
|
|
|
|
Produced by Haddock version 2.6.1 |