|
Agda.Syntax.Abstract.Name |
|
|
Description |
Abstract names should carry unique identifiers and stuff. Not right now though.
|
|
Synopsis |
|
|
|
Documentation |
|
|
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.
| Constructors | |
|
|
|
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.
| Constructors | |
|
|
|
A module name is just a qualified name.
The SetRange instance for module names sets all individual ranges
to the given one.
| Constructors | |
|
|
|
Ambiguous qualified names. Used for overloaded constructors.
Invariant: All the names in the list must have the same concrete,
unqualified name.
| Constructors | |
|
|
|
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.
|
|
|
Like withRangesOf, but uses the name parts (qualifier + name)
of the qualified name as the list of concrete names.
|
|
|
|
|
|
|
The Range sets the definition site of the name, not the use
site.
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
Is the name an operator?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Get the next version of the concrete name. For instance, nextName x = x'.
The name must not be a NoName.
|
|
Produced by Haddock version 2.6.0 |