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

Safe HaskellNone




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.