| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Compiler.MAlonzo.Encode

Synopsis

encodeModuleName :: Module -> Module
tests :: IO Bool

Documentation

encodeModuleName :: Module -> Module | Source

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.

tests :: IO Bool | Source

All the properties.
Produced by Haddock version 2.4.2