Agda.Syntax.Concrete.Name

data Name

data NamePart

data QName

data TopLevelModuleName

Operations on Name and NamePart

nameToRawName

nameParts

nameStringParts

stringNameParts

isOperator

isHole

isPrefix

isPostfix

isInfix

isNonfix

Operations on qualified names

qualify

unqualify

qnameParts

Operations on TopLevelModuleName

toTopLevelModuleName

moduleNameToFileName

projectRoot

No name stuff

noName_

noName

class IsNoName a

Showing names

Printing names

QuickCheck instances

Range instances