Agda- A dependently typed functional programming language and proof assistant

Safe HaskellSafe-Infered




encodeModuleName :: ModuleName -> ModuleNameSource

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 BoolSource

All the properties.