Agda-2.7.0: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Compiler.MAlonzo.Encode

Synopsis

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.