Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Compiler.MAlonzo.Encode
Synopsis
encodeModuleName :: ModuleName -> ModuleName
tests :: IO Bool
Documentation
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.
Produced by Haddock version 2.6.1