Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Syntax.Abstract.Name

Description

Abstract names carry unique identifiers and stuff.

Synopsis

- class MkName a where
  - mkName :: Range -> NameId -> a -> Name
  - mkName_ :: NameId -> a -> Name
- class IsProjP a where
  - isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName)
- data Suffix
  - = NoSuffix
  - | Suffix !Integer
- newtype AmbiguousQName = AmbQ {
  - unAmbQ :: List1 QName
  }
- newtype ModuleName = MName {
  - mnameToList :: [Name]
  }
- data QNamed a = QNamed {
  - qname :: QName
  - qnamed :: a
  }
- data QName = QName {
  - qnameModule :: ModuleName
  - qnameName :: Name
  }
- data Name = Name {
  - nameId :: !NameId
  - nameConcrete :: Name
  - nameCanonical :: Name
  - nameBindingSite :: Range
  - nameFixity :: Fixity'
  - nameIsRecordName :: Bool
  }
- uglyShowName :: Name -> String
- unambiguous :: QName -> AmbiguousQName
- headAmbQ :: AmbiguousQName -> QName
- isAmbiguous :: AmbiguousQName -> Bool
- getUnambiguous :: AmbiguousQName -> Maybe QName
- isAnonymousModuleName :: ModuleName -> Bool
- withRangesOf :: ModuleName -> List1 Name -> ModuleName
- withRangesOfQ :: ModuleName -> QName -> ModuleName
- mnameFromList :: [Name] -> ModuleName
- mnameFromList1 :: List1 Name -> ModuleName
- mnameToList1 :: ModuleName -> List1 Name
- noModuleName :: ModuleName
- commonParentModule :: ModuleName -> ModuleName -> ModuleName
- makeName :: NameId -> Name -> Range -> Fixity' -> Bool -> Name
- qnameToList0 :: QName -> [Name]
- qnameToList :: QName -> List1 Name
- qnameFromList :: List1 Name -> QName
- qnameToMName :: QName -> ModuleName
- mnameToQName :: ModuleName -> QName
- showQNameId :: QName -> String
- qnameToConcrete :: QName -> QName
- mnameToConcrete :: ModuleName -> QName
- toTopLevelModuleName :: ModuleName -> TopLevelModuleName
- qualifyM :: ModuleName -> ModuleName -> ModuleName
- qualifyQ :: ModuleName -> QName -> QName
- qualify :: ModuleName -> Name -> QName
- qualify_ :: Name -> QName
- isOperator :: QName -> Bool
- isLeParentModuleOf :: ModuleName -> ModuleName -> Bool
- isLtParentModuleOf :: ModuleName -> ModuleName -> Bool
- isLeChildModuleOf :: ModuleName -> ModuleName -> Bool
- isLtChildModuleOf :: ModuleName -> ModuleName -> Bool
- isInModule :: QName -> ModuleName -> Bool
- nextName :: FreshNameMode -> Name -> Name
- sameRoot :: Name -> Name -> Bool
- lensQNameName :: Lens' Name QName
- nameToArgName :: Name -> ArgName
- namedArgName :: NamedArg Name -> ArgName
- class IsNoName a where
  - isNoName :: a -> Bool
- data FreshNameMode
  - = UnicodeSubscript
  - | AsciiCounter

# Documentation

class MkName a where Source #

Make a `Name` from some kind of string.

Minimal complete definition

mkName

Methods

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

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

mkName_ :: NameId -> a -> Name Source #

#### Instances

Instances details

MkName String Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods mkName :: Range -> NameId -> String -> Name Source # mkName_ :: NameId -> String -> Name Source #

class IsProjP a where Source #

Check whether we are a projection pattern.

Methods

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

#### Instances

Instances details

IsProjP Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP Void Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Void -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP a => IsProjP (Arg a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP a => IsProjP (Named n a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) Source #

data Suffix Source #

A name suffix

Constructors

NoSuffix |
Suffix !Integer |

#### Instances

Instances details

KillRange Suffix Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT Suffix Source #
EmbPrj Suffix Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Suffix -> S Int32 Source # icod_ :: Suffix -> S Int32 Source # value :: Int32 -> R Suffix Source #
Pretty Suffix Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: Suffix -> Doc Source # prettyPrec :: Int -> Suffix -> Doc Source # prettyList :: [Suffix] -> Doc Source #
Data Suffix Source # |

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Suffix -> c Suffix Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Suffix Source #

toConstr :: Suffix -> Constr Source #

dataTypeOf :: Suffix -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Suffix) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Suffix) Source #

gmapT :: (forall b. Data b => b -> b) -> Suffix -> Suffix Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Suffix -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Suffix -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Suffix -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Suffix -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Suffix -> m Suffix Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Suffix -> m Suffix Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Suffix -> m Suffix Source #

Show Suffix Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> Suffix -> ShowS Source # show :: Suffix -> String Source # showList :: [Suffix] -> ShowS Source #
NFData Suffix Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods rnf :: Suffix -> () Source #
Eq Suffix Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods (==) :: Suffix -> Suffix -> Bool Source # (/=) :: Suffix -> Suffix -> Bool Source #
Ord Suffix Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods compare :: Suffix -> Suffix -> Ordering Source # (<) :: Suffix -> Suffix -> Bool Source # (<=) :: Suffix -> Suffix -> Bool Source # (>) :: Suffix -> Suffix -> Bool Source # (>=) :: Suffix -> Suffix -> Bool Source # max :: Suffix -> Suffix -> Suffix Source # min :: Suffix -> Suffix -> Suffix Source #

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

Constructors

AmbQ |

Fields

- unAmbQ :: List1 QName

#### Instances

Instances details

NumHoles AmbiguousQName Source # | We can have an instance for ambiguous names as all share a common concrete name.
Instance details Defined in Agda.Syntax.Abstract.Name Methods numHoles :: AmbiguousQName -> Int Source #
NamesIn AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn' :: Monoid m => (QName -> m) -> AmbiguousQName -> m Source #
HasRange AmbiguousQName Source # | The range of an `AmbiguousQName` is the range of any of its disambiguations (they are the same concrete name).
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: AmbiguousQName -> Range Source #
KillRange AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT AmbiguousQName Source #
EmbPrj AmbiguousQName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: AmbiguousQName -> S Int32 Source # icod_ :: AmbiguousQName -> S Int32 Source # value :: Int32 -> R AmbiguousQName Source #
Pretty AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: AmbiguousQName -> Doc Source # prettyPrec :: Int -> AmbiguousQName -> Doc Source # prettyList :: [AmbiguousQName] -> Doc Source #
Data AmbiguousQName Source # |

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AmbiguousQName -> c AmbiguousQName Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AmbiguousQName Source #

toConstr :: AmbiguousQName -> Constr Source #

dataTypeOf :: AmbiguousQName -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AmbiguousQName) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AmbiguousQName) Source #

gmapT :: (forall b. Data b => b -> b) -> AmbiguousQName -> AmbiguousQName Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AmbiguousQName -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AmbiguousQName -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> AmbiguousQName -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> AmbiguousQName -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AmbiguousQName -> m AmbiguousQName Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AmbiguousQName -> m AmbiguousQName Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AmbiguousQName -> m AmbiguousQName Source #

Show AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> AmbiguousQName -> ShowS Source # show :: AmbiguousQName -> String Source # showList :: [AmbiguousQName] -> ShowS Source #
NFData AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods rnf :: AmbiguousQName -> () Source #
Eq AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods (==) :: AmbiguousQName -> AmbiguousQName -> Bool Source # (/=) :: AmbiguousQName -> AmbiguousQName -> Bool Source #
Ord AmbiguousQName Source # |

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: AmbiguousQName -> AmbiguousQName -> Ordering Source #

(<) :: AmbiguousQName -> AmbiguousQName -> Bool Source #

(<=) :: AmbiguousQName -> AmbiguousQName -> Bool Source #

(>) :: AmbiguousQName -> AmbiguousQName -> Bool Source #

(>=) :: AmbiguousQName -> AmbiguousQName -> Bool Source #

max :: AmbiguousQName -> AmbiguousQName -> AmbiguousQName Source #

min :: AmbiguousQName -> AmbiguousQName -> AmbiguousQName Source #

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.

Constructors

MName |

Fields

- mnameToList :: [Name]

#### Instances

Instances details

SubstExpr ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName Source #
ExprLike ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m ModuleName Source # foldExpr :: FoldExprFn m ModuleName Source # traverseExpr :: TraverseExprFn m ModuleName Source # mapExpr :: (Expr -> Expr) -> ModuleName -> ModuleName Source #
HasRange ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: ModuleName -> Range Source #
KillRange ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT ModuleName Source #
KillRange Sections Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Sections Source #
SetRange ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> ModuleName -> ModuleName Source #
SetBindingSite ModuleName Source # | Sets the binding site of all names in the path.
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> ModuleName -> ModuleName Source #
ToConcrete ModuleName Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs ModuleName Source # Methods toConcrete :: ModuleName -> AbsToCon (ConOfAbs ModuleName) Source # bindToConcrete :: ModuleName -> (ConOfAbs ModuleName -> AbsToCon b) -> AbsToCon b Source #
PrettyTCM ModuleName Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ModuleName -> m Doc Source #
InstantiateFull ModuleName Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ModuleName -> ReduceM ModuleName Source #
EmbPrj ModuleName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ModuleName -> S Int32 Source # icod_ :: ModuleName -> S Int32 Source # value :: Int32 -> R ModuleName Source #
Pretty ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: ModuleName -> Doc Source # prettyPrec :: Int -> ModuleName -> Doc Source # prettyList :: [ModuleName] -> Doc Source #
Sized ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods size :: ModuleName -> Int Source #
Data ModuleName Source # |

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleName -> c ModuleName Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleName Source #

toConstr :: ModuleName -> Constr Source #

dataTypeOf :: ModuleName -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleName) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleName) Source #

gmapT :: (forall b. Data b => b -> b) -> ModuleName -> ModuleName Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleName -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleName -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ModuleName -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleName -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleName -> m ModuleName Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleName -> m ModuleName Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleName -> m ModuleName Source #

Show ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> ModuleName -> ShowS Source # show :: ModuleName -> String Source # showList :: [ModuleName] -> ShowS Source #
NFData ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods rnf :: ModuleName -> () Source #
Eq ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods (==) :: ModuleName -> ModuleName -> Bool Source # (/=) :: ModuleName -> ModuleName -> Bool Source #
Ord ModuleName Source # |

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: ModuleName -> ModuleName -> Ordering Source #

(<) :: ModuleName -> ModuleName -> Bool Source #

(<=) :: ModuleName -> ModuleName -> Bool Source #

(>) :: ModuleName -> ModuleName -> Bool Source #

(>=) :: ModuleName -> ModuleName -> Bool Source #

max :: ModuleName -> ModuleName -> ModuleName Source #

min :: ModuleName -> ModuleName -> ModuleName Source #

type ConOfAbs ModuleName Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs ModuleName = QName

data QNamed a Source #

Something preceeded by a qualified name.

Constructors

QNamed |

Fields

- qname :: QName
- qnamed :: a

#### Instances

Instances details

Foldable QNamed Source # |

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

fold :: Monoid m => QNamed m -> m Source #

foldMap :: Monoid m => (a -> m) -> QNamed a -> m Source #

foldMap' :: Monoid m => (a -> m) -> QNamed a -> m Source #

foldr :: (a -> b -> b) -> b -> QNamed a -> b Source #

foldr' :: (a -> b -> b) -> b -> QNamed a -> b Source #

foldl :: (b -> a -> b) -> b -> QNamed a -> b Source #

foldl' :: (b -> a -> b) -> b -> QNamed a -> b Source #

foldr1 :: (a -> a -> a) -> QNamed a -> a Source #

foldl1 :: (a -> a -> a) -> QNamed a -> a Source #

toList :: QNamed a -> [a] Source #

null :: QNamed a -> Bool Source #

length :: QNamed a -> Int Source #

elem :: Eq a => a -> QNamed a -> Bool Source #

maximum :: Ord a => QNamed a -> a Source #

minimum :: Ord a => QNamed a -> a Source #

sum :: Num a => QNamed a -> a Source #

product :: Num a => QNamed a -> a Source #

Traversable QNamed Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods traverse :: Applicative f => (a -> f b) -> QNamed a -> f (QNamed b) Source # sequenceA :: Applicative f => QNamed (f a) -> f (QNamed a) Source # mapM :: Monad m => (a -> m b) -> QNamed a -> m (QNamed b) Source # sequence :: Monad m => QNamed (m a) -> m (QNamed a) Source #
Functor QNamed Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods fmap :: (a -> b) -> QNamed a -> QNamed b Source # (<$) :: a -> QNamed b -> QNamed a Source #
Reify (QNamed Clause) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (QNamed Clause) Source # Methods reify :: MonadReify m => QNamed Clause -> m (ReifiesTo (QNamed Clause)) Source # reifyWhen :: MonadReify m => Bool -> QNamed Clause -> m (ReifiesTo (QNamed Clause)) Source #
Reify (QNamed System) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (QNamed System) Source # Methods reify :: MonadReify m => QNamed System -> m (ReifiesTo (QNamed System)) Source # reifyWhen :: MonadReify m => Bool -> QNamed System -> m (ReifiesTo (QNamed System)) Source #
ToAbstract (QNamed Clause) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (QNamed Clause) Source # Methods toAbstract :: MonadReflectedToAbstract m => QNamed Clause -> m (AbsOfRef (QNamed Clause)) Source #
ToAbstract (List1 (QNamed Clause)) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (List1 (QNamed Clause)) Source # Methods toAbstract :: MonadReflectedToAbstract m => List1 (QNamed Clause) -> m (AbsOfRef (List1 (QNamed Clause))) Source #
ToAbstract [QNamed Clause] Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef [QNamed Clause] Source # Methods toAbstract :: MonadReflectedToAbstract m => [QNamed Clause] -> m (AbsOfRef [QNamed Clause]) Source #
PrettyTCM (QNamed Clause) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => QNamed Clause -> m Doc Source #
Pretty a => Pretty (QNamed a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: QNamed a -> Doc Source # prettyPrec :: Int -> QNamed a -> Doc Source # prettyList :: [QNamed a] -> Doc Source #
Show a => Show (QNamed a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> QNamed a -> ShowS Source # show :: QNamed a -> String Source # showList :: [QNamed a] -> ShowS Source #
type ReifiesTo (QNamed Clause) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (QNamed Clause) = Clause
type ReifiesTo (QNamed System) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (QNamed System) = [Clause]
type AbsOfRef (QNamed Clause) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (QNamed Clause) = Clause
type AbsOfRef (List1 (QNamed Clause)) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (List1 (QNamed Clause)) = List1 Clause
type AbsOfRef [QNamed Clause] Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef [QNamed Clause] = [Clause]

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.

Constructors

QName |

Fields

- qnameModule :: ModuleName
- qnameName :: Name

#### Instances

Instances details

DeclaredNames RecordDirectives Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => RecordDirectives -> m Source #
DeclaredNames KName Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => KName -> m Source #
ExprLike QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m QName Source # foldExpr :: FoldExprFn m QName Source # traverseExpr :: TraverseExprFn m QName Source # mapExpr :: (Expr -> Expr) -> QName -> QName Source #
LensFixity QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensFixity :: Lens' Fixity QName Source #
LensFixity' QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensFixity' :: Lens' Fixity' QName Source #
LensInScope QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensInScope :: Lens' NameInScope QName Source # isInScope :: QName -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> QName -> QName Source # setInScope :: QName -> QName Source # setNotInScope :: QName -> QName Source #
NumHoles QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods numHoles :: QName -> Int Source #
TermLike QName Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> QName -> m QName Source # foldTerm :: Monoid m => (Term -> m) -> QName -> m Source #
NamesIn QName Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn' :: Monoid m => (QName -> m) -> QName -> m Source #
HasRange QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: QName -> Range Source #
KillRange QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT QName Source #
KillRange Definitions Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Definitions Source #
KillRange RewriteRuleMap Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT RewriteRuleMap Source #
SetRange QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> QName -> QName Source #
SetBindingSite QName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> QName -> QName Source #
ToConcrete QName Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs QName Source # Methods toConcrete :: QName -> AbsToCon (ConOfAbs QName) Source # bindToConcrete :: QName -> (ConOfAbs QName -> AbsToCon b) -> AbsToCon b Source #
Occurs QName Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: QName -> OccursM QName Source # metaOccurs :: MetaId -> QName -> TCM () Source #
PrettyTCM QName Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => QName -> m Doc Source #
FromTerm QName Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction QName) Source #
PrimTerm QName Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: QName -> TCM Term Source #
PrimType QName Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primType :: QName -> TCM Type Source #
ToTerm QName Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (QName -> Term) Source # toTermR :: TCM (QName -> ReduceM Term) Source #
InstantiateFull QName Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: QName -> ReduceM QName Source #
EmbPrj QName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QName -> S Int32 Source # icod_ :: QName -> S Int32 Source # value :: Int32 -> R QName Source #
Subst QName Source # |
Instance details Defined in Agda.TypeChecking.Substitute.Class Associated Types type SubstArg QName Source # Methods applySubst :: Substitution' (SubstArg QName) -> QName -> QName Source #
Unquote QName Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM QName Source #
Pretty QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: QName -> Doc Source # prettyPrec :: Int -> QName -> Doc Source # prettyList :: [QName] -> Doc Source #
Sized QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods size :: QName -> Int Source #
Data QName Source # |

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QName -> c QName Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QName Source #

toConstr :: QName -> Constr Source #

dataTypeOf :: QName -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QName) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QName) Source #

gmapT :: (forall b. Data b => b -> b) -> QName -> QName Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> QName -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> QName -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> QName -> m QName Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QName -> m QName Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QName -> m QName Source #

Show QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> QName -> ShowS Source # show :: QName -> String Source # showList :: [QName] -> ShowS Source #
NFData QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods rnf :: QName -> () Source #
Eq QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods (==) :: QName -> QName -> Bool Source # (/=) :: QName -> QName -> Bool Source #
Ord QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods compare :: QName -> QName -> Ordering Source # (<) :: QName -> QName -> Bool Source # (<=) :: QName -> QName -> Bool Source # (>) :: QName -> QName -> Bool Source # (>=) :: QName -> QName -> Bool Source # max :: QName -> QName -> QName Source # min :: QName -> QName -> QName Source #
Hashable QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods hashWithSalt :: Int -> QName -> Int Source # hash :: QName -> Int Source #
Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #
Conversion TOM Term (MExp O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) Source #
Conversion TOM Type (MExp O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) Source #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #
Conversion MOT (Exp O) Term Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Term Source #
Conversion MOT (Exp O) Type Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Type Source #
Conversion TOM (Arg Pattern) (Pat O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg Pattern -> TOM (Pat O) Source #
Conversion TOM [Clause] [([Pat O], MExp O)] Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #
Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: MM a (RefInfo O) -> MOT b Source #
ToConcrete (Maybe QName) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Maybe QName) Source # Methods toConcrete :: Maybe QName -> AbsToCon (ConOfAbs (Maybe QName)) Source # bindToConcrete :: Maybe QName -> (ConOfAbs (Maybe QName) -> AbsToCon b) -> AbsToCon b Source #
type ConOfAbs QName Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs QName = QName
type SubstArg QName Source # |
Instance details Defined in Agda.TypeChecking.Substitute.Class type SubstArg QName = Term
type ConOfAbs (Maybe QName) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Maybe QName) = Maybe Name

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.

Constructors

Name |

Fields

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

#### Instances

Instances details

LensFixity Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensFixity :: Lens' Fixity Name Source #
LensFixity' Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensFixity' :: Lens' Fixity' Name Source #
IsNoName Name Source # | An abstract name is empty if its concrete name is empty.
Instance details Defined in Agda.Syntax.Abstract.Name Methods isNoName :: Name -> Bool Source #
LensInScope Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensInScope :: Lens' NameInScope Name Source # isInScope :: Name -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> Name -> Name Source # setInScope :: Name -> Name Source # setNotInScope :: Name -> Name Source #
NumHoles Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods numHoles :: Name -> Int Source #
Suggest Name Source # |
Instance details Defined in Agda.Syntax.Internal Methods suggestName :: Name -> Maybe String Source #
HasRange Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: Name -> Range Source #
KillRange Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT Name Source #
SetRange Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> Name -> Name Source #
SetBindingSite Name Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> Name -> Name Source #
ToConcrete Name Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs Name Source # Methods toConcrete :: Name -> AbsToCon (ConOfAbs Name) Source # bindToConcrete :: Name -> (ConOfAbs Name -> AbsToCon b) -> AbsToCon b Source #
Reify Name Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo Name Source # Methods reify :: MonadReify m => Name -> m (ReifiesTo Name) Source # reifyWhen :: MonadReify m => Bool -> Name -> m (ReifiesTo Name) Source #
AddContext Name Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Name -> m a -> m a Source # contextSize :: Name -> Nat Source #
PrettyTCM Name Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Name -> m Doc Source #
InstantiateFull Name Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Name -> ReduceM Name Source #
EmbPrj Name Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Name -> S Int32 Source # icod_ :: Name -> S Int32 Source # value :: Int32 -> R Name Source #
Subst Name Source # |
Instance details Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg Name Source # Methods applySubst :: Substitution' (SubstArg Name) -> Name -> Name Source #
Pretty Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: Name -> Doc Source # prettyPrec :: Int -> Name -> Doc Source # prettyList :: [Name] -> Doc Source #
Data Name Source # |

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Name -> c Name Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Name Source #

toConstr :: Name -> Constr Source #

dataTypeOf :: Name -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Name) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name) Source #

gmapT :: (forall b. Data b => b -> b) -> Name -> Name Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Name -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Name -> m Name Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name Source #

Show Name Source # | Use `prettyShow` to print names to the user.
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> Name -> ShowS Source # show :: Name -> String Source # showList :: [Name] -> ShowS Source #
NFData Name Source # | The range is not forced.
Instance details Defined in Agda.Syntax.Abstract.Name Methods rnf :: Name -> () Source #
Eq Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods (==) :: Name -> Name -> Bool Source # (/=) :: Name -> Name -> Bool Source #
Ord Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods compare :: Name -> Name -> Ordering Source # (<) :: Name -> Name -> Bool Source # (<=) :: Name -> Name -> Bool Source # (>) :: Name -> Name -> Bool Source # (>=) :: Name -> Name -> Bool Source # max :: Name -> Name -> Name Source # min :: Name -> Name -> Name Source #
Hashable Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods hashWithSalt :: Int -> Name -> Int Source # hash :: Name -> Int Source #
AddContext (Dom (Name, Type)) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a Source # contextSize :: Dom (Name, Type) -> Nat Source #
PrettyTCM (Dom (Name, Type)) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Dom (Name, Type) -> m Doc Source #
(ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Dom r, Name) Source # Methods toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m (AbsOfRef (Dom r, Name)) Source #
AddContext (Name, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a Source # contextSize :: (Name, Dom Type) -> Nat Source #
AddContext (List1 Name, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 Name, Dom Type) -> m a -> m a Source # contextSize :: (List1 Name, Dom Type) -> Nat Source #
AddContext (List1 (Arg Name), Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (Arg Name), Type) -> m a -> m a Source # contextSize :: (List1 (Arg Name), Type) -> Nat Source #
AddContext (List1 (NamedArg Name), Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (NamedArg Name), Type) -> m a -> m a Source # contextSize :: (List1 (NamedArg Name), Type) -> Nat Source #
AddContext (List1 (WithHiding Name), Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (WithHiding Name), Dom Type) -> m a -> m a Source # contextSize :: (List1 (WithHiding Name), Dom Type) -> Nat Source #
AddContext ([Name], Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a Source # contextSize :: ([Name], Dom Type) -> Nat Source #
AddContext ([Arg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source # contextSize :: ([Arg Name], Type) -> Nat Source #
AddContext ([NamedArg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # contextSize :: ([NamedArg Name], Type) -> Nat Source #
AddContext ([WithHiding Name], Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source #
type ConOfAbs Name Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Name = Name
type ReifiesTo Name Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Name = Name
type SubstArg Name Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Name = Term
type AbsOfRef (Dom r, Name) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Dom r, Name) = TypedBinding

uglyShowName :: Name -> String Source #

Useful for debugging scoping problems

unambiguous :: QName -> AmbiguousQName Source #

A singleton "ambiguous" name.

headAmbQ :: AmbiguousQName -> QName Source #

Get the first of the ambiguous names.

isAmbiguous :: AmbiguousQName -> Bool Source #

Is a name ambiguous.

getUnambiguous :: AmbiguousQName -> Maybe QName Source #

Get the name if unambiguous.

isAnonymousModuleName :: ModuleName -> Bool Source #

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

withRangesOf :: ModuleName -> List1 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.

mnameFromList :: [Name] -> ModuleName Source #

mnameFromList1 :: List1 Name -> ModuleName Source #

mnameToList1 :: ModuleName -> List1 Name Source #

noModuleName :: ModuleName Source #

commonParentModule :: ModuleName -> ModuleName -> ModuleName Source #

makeName :: NameId -> Name -> Range -> Fixity' -> Bool -> Name Source #

qnameToList0 :: QName -> [Name] Source #

qnameToList :: QName -> List1 Name Source #

qnameFromList :: List1 Name -> QName Source #

qnameToMName :: QName -> ModuleName Source #

mnameToQName :: ModuleName -> QName Source #

showQNameId :: QName -> String 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.

mnameToConcrete :: ModuleName -> QName Source #

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.

qualifyM :: ModuleName -> ModuleName -> ModuleName Source #

qualifyQ :: ModuleName -> QName -> QName Source #

qualify :: ModuleName -> Name -> QName Source #

qualify_ :: Name -> QName Source #

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

isOperator :: QName -> Bool Source #

Is the name an operator?

isLeParentModuleOf :: ModuleName -> ModuleName -> Bool Source #

Is the first module a weak parent of the second?

isLtParentModuleOf :: ModuleName -> ModuleName -> Bool Source #

Is the first module a proper parent of the second?

isLeChildModuleOf :: ModuleName -> ModuleName -> Bool Source #

Is the first module a weak child of the second?

isLtChildModuleOf :: ModuleName -> ModuleName -> Bool Source #

Is the first module a proper child of the second?

isInModule :: QName -> ModuleName -> Bool Source #

nextName :: FreshNameMode -> Name -> Name Source #

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

sameRoot :: Name -> Name -> Bool Source #

lensQNameName :: Lens' Name QName Source #

nameToArgName :: Name -> ArgName Source #

namedArgName :: NamedArg Name -> ArgName Source #

class IsNoName a where Source #

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

Minimal complete definition

Nothing

Methods

isNoName :: a -> Bool Source #

default isNoName :: (Foldable t, IsNoName b, t b ~ a) => a -> Bool Source #

#### Instances

Instances details

IsNoName Name Source # | An abstract name is empty if its concrete name is empty.
Instance details Defined in Agda.Syntax.Abstract.Name Methods isNoName :: Name -> Bool Source #
IsNoName Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: Name -> Bool Source #
IsNoName QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: QName -> Bool Source #
IsNoName ByteString Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: ByteString -> Bool Source #
IsNoName String Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: String -> Bool Source #
IsNoName a => IsNoName (Ranged a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: Ranged a -> Bool Source #
IsNoName a => IsNoName (WithOrigin a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: WithOrigin a -> Bool Source #

data FreshNameMode Source #

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, …