Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




Abstract names carry unique identifiers and stuff.



data Name Source

A name is a unique identifier and a suggestion for a concrete name. The concrete name contains the source location (if any) of the name. The source location of the binding site is also recorded.


Eq Name Source 
Ord Name Source 
Show Name Source

Only use this show function in debugging! To convert an abstract Name into a string use prettyShow.

CoArbitrary Name Source 
Arbitrary Name Source

The generated names all have the same Fixity': noFixity'.

Hashable Name Source 
Pretty Name Source 
KillRange Name Source 
SetRange Name Source 
HasRange Name Source 
IsNoName Name Source

An abstract name is empty if its concrete name is empty.

Subst Name Source 
AddContext Name Source 
PrettyTCM Name Source 
EmbPrj Name Source 
InstantiateFull Name Source 
ToConcrete Name Name Source 
Reify Name Name Source 
Suggest Name (Abs b) Source 
AddContext (Dom (Name, Type)) Source 
ToAbstract (NewName Name) Name Source 
ToAbstract (NewName BoundName) Name Source 
(Free i, Reify i a) => Reify (Abs i) (Name, a) Source 
AddContext ([WithHiding Name], Dom Type) Source 
AddContext ([Name], Dom Type) Source 
AddContext (Name, Dom Type) Source 

data QName Source

Qualified names are non-empty lists of names. Equality on qualified names are just equality on the last name, i.e. the module part is just for show.

The SetRange instance for qualified names sets all individual ranges (including those of the module prefix) to the given one.



data QNamed a Source

Something preceeded by a qualified name.




qname :: QName
qnamed :: a

newtype ModuleName Source

A module name is just a qualified name.

The SetRange instance for module names sets all individual ranges to the given one.




mnameToList :: [Name]

newtype AmbiguousQName Source

Ambiguous qualified names. Used for overloaded constructors.

Invariant: All the names in the list must have the same concrete, unqualified name. (This implies that they all have the same Range).




unAmbQ :: [QName]


Eq AmbiguousQName Source 
Show AmbiguousQName Source 
Pretty AmbiguousQName Source 
KillRange AmbiguousQName Source 
HasRange AmbiguousQName Source

The range of an AmbiguousQName is the range of any of its disambiguations (they are the same concrete name).

EmbPrj AmbiguousQName Source 
UniverseBi Declaration AmbiguousQName 

isAnonymousModuleName :: ModuleName -> Bool Source

A module is anonymous if the qualification path ends in an underscore.

withRangesOf :: ModuleName -> [Name] -> ModuleName Source

Sets the ranges of the individual names in the module name to match those of the corresponding concrete names. If the concrete names are fewer than the number of module name name parts, then the initial name parts get the range noRange.

C.D.E `withRangesOf` [A, B] returns C.D.E but with ranges set as follows:

  • C: noRange.
  • D: the range of A.
  • E: the range of B.

Precondition: The number of module name name parts has to be at least as large as the length of the list.

withRangesOfQ :: ModuleName -> QName -> ModuleName Source

Like withRangesOf, but uses the name parts (qualifier + name) of the qualified name as the list of concrete names.

class MkName a where Source

Make a Name from some kind of string.

Minimal complete definition



mkName :: Range -> NameId -> a -> Name Source

The Range sets the definition site of the name, not the use site.

mkName_ :: NameId -> a -> Name Source


qnameToConcrete :: QName -> QName Source

Turn a qualified name into a concrete name. This should only be used as a fallback when looking up the right concrete name in the scope fails.

toTopLevelModuleName :: ModuleName -> TopLevelModuleName Source

Computes the TopLevelModuleName corresponding to the given module name, which is assumed to represent a top-level module name.

Precondition: The module name must be well-formed.

qualify_ :: Name -> QName Source

Convert a Name to a QName (add no module name).

isOperator :: QName -> Bool Source

Is the name an operator?

nextName :: Name -> Name Source

Get the next version of the concrete name. For instance, nextName "x" = "x₁". The name must not be a NoName.

Important instances: Eq, Ord, Hashable

IsNoName instances (checking for "_")

Show instances

Pretty instances

Range instances




Sized instances

Arbitrary instances

class IsNoName a where Source

Check whether a name is the empty name "_".


isNoName :: a -> Bool Source


IsNoName String Source 
IsNoName ByteString Source 
IsNoName QName Source 
IsNoName Name Source 
IsNoName Name Source

An abstract name is empty if its concrete name is empty.