Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Compiler.MAlonzo.Encode

Synopsis

- encodeModuleName :: ModuleName -> ModuleName
- tests :: IO Bool

# Documentation

encodeModuleName :: ModuleName -> ModuleName

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

All the properties.