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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Compiler.MAlonzo.Encode

Synopsis

- encodeModuleName :: ModuleName -> ModuleName

# Documentation

encodeModuleName :: ModuleName -> ModuleName 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.