ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Abstract.Name

Abstract names carry unique identifiers and stuff.

7 types
3 classes
37 values

PackageAgda-2.7.0.1
Exports47
LanguageHaskell2010
LicenceMIT
SourceName.hs

datadata Name

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

Name
- nameId :: !NameId
- nameConcrete :: Name
  The concrete name used for this instance
- nameCanonical :: Name
  The concrete name in the original definition (needed by primShowQName, see #4735)
- nameBindingSite :: Range
- nameFixity :: Fixity'
- nameIsRecordName :: Bool
  Is this the name of the invisible record variable self? Should not be printed or displayed in the context, see issue #3584.

Instances39Eq, Ord, Show, NFData, Hashable, Pretty, …

Eq NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Ord NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Show NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Use prettyShow to print names to the user.
NFData NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
The range is not forced.
Hashable NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Pretty NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
IsNoName NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
An abstract name is empty if its concrete name is empty.
AddContext NameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
HasRange NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Subst NameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan
PrettyTCM NameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Pretty
PrettyTCM ContextEntryDefined in Agda-2.7.0.1 · Agda.TypeChecking.Pretty
Reify NameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.InternalToAbstract
ToConcrete NameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
KillRange NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
SetRange NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
LensFixity' NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
LensFixity NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
LensInScope NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
NumHoles NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Suggest NameDefined in Agda-2.7.0.1 · Agda.Syntax.Internal
SetBindingSite NameDefined in Agda-2.7.0.1 · Agda.Syntax.Scope.Base
InstantiateFull NameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Reduce
EmbPrj NameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan
AddContext (Dom (Name, Type))Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (Name, Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (List1 Name, Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (List1 (Arg Name), Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (List1 (NamedArg Name), Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (List1 (WithHiding Name), Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext ([Name], Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext ([Arg Name], Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext ([NamedArg Name], Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext ([WithHiding Name], Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
(ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
type SubstArg Name = TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan
type ReifiesTo Name = NameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.InternalToAbstract
type ConOfAbs Name = NameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
type AbsOfRef (Dom r, Name) = TypedBindingDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract

datadata QName

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

QName
- qnameModule :: ModuleName
- qnameName :: Name

Instances43Eq, Ord, Show, NFData, Hashable, Pretty, …

Eq QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Ord QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Show QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
NFData QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Hashable QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Pretty QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
HasRange QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Subst QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute.Class
PrettyTCM QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Pretty
ToConcrete RecordDirectivesDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
Hilite RecordDirectivesDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.FromAbstract
Reengineered from the old Geniplate-implemented highlighting extraction. This was the old procedure:
Traversal over declaration in abstract syntax that collects the following hiliting information:
1. constructorInfo (highest prio)
2.
theRest
(medium prio) 3.
nameInfo
(lowest prio)
nameInfo: "All names mentioned in the syntax tree (not bound variables)." For each possibly ambiguous name (QName and AmbiguousQName) that not isExtendedLambdaName, do hiliteAmbiguous (used to be calledgenerate).
constructorInfo (only when highlighting level == Full): "After the code has been type checked more information may be available for overloaded constructors, and generateConstructorInfo takes advantage of this information. Note, however, that highlighting for overloaded constructors is included also in nameInfo." This is not computed by recursion over the abstract syntax, but gets the constructor names stDisambiguatedNames that fall within the bounds of the current declaration.
theRest: Bound variables, dotted patterns, record fields, module names, the "as" and "to" symbols and some other things.
Here is a table what theRest used to collect:
- -------------------------------------------------------------------- | A.Expr
- -------------------------------------------------------------------- | getVarAndField (Expr) | A.Var | bound | getVarAndField | A.Rec(Update) | field | getExpr (Expr) | A.PatternSyn | patsyn | getExpr | A.Macro | macro
- -------------------------------------------------------------------- | A.LetBinding
- -------------------------------------------------------------------- | getLet | A.LetBind | bound | getLet | A.LetDeclaredVariable | bound
- -------------------------------------------------------------------- | A.LamBinding
- -------------------------------------------------------------------- | getLam | A.Binder under A.DomainFree | bound | getTyped | A.Binder under A.TBind | bound
- -------------------------------------------------------------------- | A.Pattern'
- -------------------------------------------------------------------- | getPattern(Syn) | A.VarP | bound | getPattern(Syn) | A.AsP | bound | getPattern(Syn) | A.DotP (not isProjP) | DottedPattern | getPattern(Syn) | A.RecP | field | getPattern(Syn) | A.PatternSynP | patsyn
- -------------------------------------------------------------------- | A.Declaration
- -------------------------------------------------------------------- | getFieldDecl | A.Field under A.RecDef | field | getPatSynArgs | A.PatternSynDef | bound | getPragma | A.BuiltinPragma... | keyword
- -------------------------------------------------------------------- | A.NamedArg (polymorphism not supported in geniplate)
- -------------------------------------------------------------------- | getNamedArg | NamedArg a | nameOf | getNamedArgE | NamedArg Exp | nameOf | getNamedArgP | NamedArg Pattern | nameOf | getNamedArgB | NamedArg BindName | nameOf | getNamedArgL | NamedArg LHSCore | nameOf
| getModuleName | A.MName | mod | getModuleInfo | ModuleInfo | asName, (range of as,to) | getQuantityAttr | Common.Quantity | Symbol (if range)
Hilite QNameDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.FromAbstract
KillRange QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
KillRange DefinitionsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
KillRange RewriteRuleMapDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
SetRange QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
LensFixity' QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
LensFixity QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
LensInScope QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
NumHoles QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Sized QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
DeclaredNames RecordDirectivesDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
DeclaredNames KNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
TermLike QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Generic
NamesIn QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Names
SetBindingSite QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Scope.Base
LivesInCurrentModule QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
Occurs QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
FromTerm QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimType QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
InstantiateFull QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Reduce
EmbPrj QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Unquote QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Unquote
Collection KName NameKindBuilderDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.Generate
Singleton KName NameKindBuilderDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.Generate
Hilite (RenamingTo QName)Defined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.FromAbstract
type SubstArg QName = TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute.Class
type ConOfAbs RecordDirectives = [RecordDirective]Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
type ConOfAbs QName = QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete

newtypenewtype ModuleName

A module name is just a qualified name.

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

Constructors

MName
- mnameToList :: [Name]

Instances22Eq, Ord, Show, NFData, Pretty, HasRange, …

Eq ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Ord ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Show ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
NFData ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Pretty ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
HasRange ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
PrettyTCM ModuleNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Pretty
ToConcrete ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
Hilite ModuleNameDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.FromAbstract
SubstExpr ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract
KillRange ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
KillRange SectionsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
SetRange ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Sized ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
BoundAndUsed ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.UsedNames
ExprLike ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
SetBindingSite ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Scope.Base
Sets the binding site of all names in the path.
BlankVars ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.InternalToAbstract
InstantiateFull ModuleNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Reduce
EmbPrj ModuleNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Hilite (RenamingTo ModuleName)Defined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.FromAbstract
type ConOfAbs ModuleName = QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete

classclass IsProjP a where

Check whether we are a projection pattern.

Methods

isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName)

Instances6IsProjP

IsProjP ExprDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract
IsProjP VoidDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
IsProjP (Pattern' e)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract
IsProjP (Pattern' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal
IsProjP a => IsProjP (Arg a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
IsProjP a => IsProjP (Named n a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name

datadata Suffix

A name suffix

Constructors

NoSuffix
Suffix !Integer

Instances7Eq, Ord, Show, NFData, Pretty, KillRange, …

Eq SuffixDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Ord SuffixDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Show SuffixDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
NFData SuffixDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Pretty SuffixDefined in Agda-2.7.0.1 · Agda.Syntax.Scope.Base · orphan
KillRange SuffixDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract · orphan
EmbPrj SuffixDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Abstract · orphan

datadata QNamed a

Something preceeded by a qualified name.

Constructors

QNamed
- qname :: QName
- qnamed :: a

Instances16Functor, Foldable, Traversable, Show, Pretty, PrettyTCM, …

Functor QNamedDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Foldable QNamedDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Traversable QNamedDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Show a => Show (QNamed a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Pretty a => Pretty (QNamed a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
PrettyTCM (QNamed Clause)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Pretty
Reify (QNamed Clause)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.InternalToAbstract
Reify (QNamed System)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.InternalToAbstract
ToAbstract (QNamed Clause)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract (List1 (QNamed Clause))Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract [QNamed Clause]Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
type ReifiesTo (QNamed Clause) = ClauseDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.InternalToAbstract
type ReifiesTo (QNamed System) = [Clause]Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.InternalToAbstract
type AbsOfRef (QNamed Clause) = ClauseDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
type AbsOfRef (List1 (QNamed Clause)) = List1 ClauseDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
type AbsOfRef [QNamed Clause] = [Clause]Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract

valuenextName :: FreshNameMode -> Name -> Name

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

valuequalify :: ModuleName -> Name -> QName

valueunambiguous :: QName -> AmbiguousQName

A singleton "ambiguous" name.

classclass MkName a where

Make a Name from some kind of string.

Methods

mkName :: Range -> NameId -> a -> Name
The Range sets the definition site of the name, not the use site.
mkName_ :: NameId -> a -> Name

Instances1MkName

MkName StringDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name

valueisOperator :: QName -> Bool

Is the name an operator?

valuesameRoot :: Name -> Name -> Bool

valuelensQNameName :: Lens' QName Name

valueuglyShowName :: Name -> String

Useful for debugging scoping problems

newtypenewtype AmbiguousQName

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

Constructors

AmbQ
- unAmbQ :: List1 QName

Instances11Eq, Ord, Show, NFData, Pretty, HasRange, …

Eq AmbiguousQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Ord AmbiguousQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Show AmbiguousQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
NFData AmbiguousQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Pretty AmbiguousQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
HasRange AmbiguousQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
The range of an AmbiguousQName is the range of any of its disambiguations (they are the same concrete name).
Hilite AmbiguousQNameDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.FromAbstract
KillRange AmbiguousQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
NumHoles AmbiguousQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
We can have an instance for ambiguous names as all share a common concrete name.
NamesIn AmbiguousQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Names
EmbPrj AmbiguousQNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan

valueheadAmbQ :: AmbiguousQName -> QName

Get the first of the ambiguous names.

valueisAmbiguous :: AmbiguousQName -> Bool

Is a name ambiguous.

valuegetUnambiguous :: AmbiguousQName -> Maybe QName

Get the name if unambiguous.

valueisAnonymousModuleName :: ModuleName -> Bool

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

valuewithRangesOf :: ModuleName -> List1 Name -> ModuleName

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.

valuewithRangesOfQ :: ModuleName -> QName -> ModuleName

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

valuemnameFromList :: [Name] -> ModuleName

valuemnameFromList1 :: List1 Name -> ModuleName

valuemnameToList1 :: ModuleName -> List1 Name

valuenoModuleName :: ModuleName

valuecommonParentModule :: ModuleName -> ModuleName -> ModuleName

valuemakeName :: NameId -> Name -> Range -> Fixity' -> Bool -> Name

valueqnameToList0 :: QName -> [Name]

valueqnameToList :: QName -> List1 Name

valueqnameFromList :: List1 Name -> QName

valueqnameToMName :: QName -> ModuleName

valuemnameToQName :: ModuleName -> QName

valueshowQNameId :: QName -> String

valueqnameToConcrete :: QName -> QName

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.

valuemnameToConcrete :: ModuleName -> QName

valuequalifyM :: ModuleName -> ModuleName -> ModuleName

valuequalifyQ :: ModuleName -> QName -> QName

valuequalify_ :: Name -> QName

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

valueisLeParentModuleOf :: ModuleName -> ModuleName -> Bool

Is the first module a weak parent of the second?

valueisLtParentModuleOf :: ModuleName -> ModuleName -> Bool

Is the first module a proper parent of the second?

valueisLeChildModuleOf :: ModuleName -> ModuleName -> Bool

Is the first module a weak child of the second?

valueisLtChildModuleOf :: ModuleName -> ModuleName -> Bool

Is the first module a proper child of the second?

valueisInModule :: QName -> ModuleName -> Bool

valuenameToArgName :: Name -> ArgName

valuenamedArgName :: NamedArg Name -> ArgName

classclass IsNoName a where

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

Methods

isNoName :: a -> Bool

Instances8IsNoName, …

IsNoName NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
An abstract name is empty if its concrete name is empty.
IsNoName NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
IsNoName QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
IsNoName RawTopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName
IsNoName ByteStringDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
IsNoName StringDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
IsNoName a => IsNoName (Ranged a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
IsNoName a => IsNoName (WithOrigin a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name

datadata FreshNameMode

Method by which to generate fresh unshadowed names.

Constructors

UnicodeSubscript
Append an integer Unicode subscript: x, x₁, x₂, …
AsciiCounter
Append an integer ASCII counter: x, x1, x2, …