Agda-2.2.4: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Compiler.MAlonzo.Encode
Synopsis
encodeModuleName :: Module -> Module
tests :: IO Bool
Documentation
encodeModuleName :: Module -> ModuleSource

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 often preserves names. The function always preserves .s.

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.4.2