Agda.Syntax.Abstract.Name

Abstract names carry unique identifiers and stuff.

Documentation

class MkName a where

Make a Name from some kind of string.

Minimal complete definition

mkName

Methods

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

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

mkName_ :: NameId -> a -> Name

Instances

MkName String

Defined in Agda.Syntax.Abstract.Name

Methods

mkName :: Range -> NameId -> String -> Name

mkName_ :: NameId -> String -> Name

class IsProjP a where

Check whether we are a projection pattern.

Minimal complete definition

isProjP

Methods

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

Instances

IsProjP Void

Defined in Agda.Syntax.Abstract.Name

Methods

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

IsProjP Expr

Defined in Agda.Syntax.Abstract

Methods

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

IsProjP a => IsProjP (Arg a)

Defined in Agda.Syntax.Abstract.Name

Methods

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

IsProjP (Pattern' a)

Defined in Agda.Syntax.Internal

Methods

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

IsProjP (Pattern' e)

Defined in Agda.Syntax.Abstract

Methods

isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName)

IsProjP a => IsProjP (Named n a)

Defined in Agda.Syntax.Abstract.Name

Methods

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

newtype 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

Fields

• unAmbQ :: NonemptyList QName

Instances

Eq AmbiguousQName

Defined in Agda.Syntax.Abstract.Name

Methods

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

(/=) :: AmbiguousQName -> AmbiguousQName -> Bool

Data AmbiguousQName

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

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

toConstr :: AmbiguousQName -> Constr

dataTypeOf :: AmbiguousQName -> DataType

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

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

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

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

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

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

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

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

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

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

Ord AmbiguousQName

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: AmbiguousQName -> AmbiguousQName -> Ordering

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

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

(>) :: AmbiguousQName -> AmbiguousQName -> Bool

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

max :: AmbiguousQName -> AmbiguousQName -> AmbiguousQName

min :: AmbiguousQName -> AmbiguousQName -> AmbiguousQName

Show AmbiguousQName

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> AmbiguousQName -> ShowS

show :: AmbiguousQName -> String

showList :: [AmbiguousQName] -> ShowS

Pretty AmbiguousQName

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: AmbiguousQName -> Doc

prettyPrec :: Int -> AmbiguousQName -> Doc

prettyList :: [AmbiguousQName] -> Doc

KillRange AmbiguousQName

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT AmbiguousQName

HasRange AmbiguousQName

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

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: AmbiguousQName -> Range

NumHoles AmbiguousQName

We can have an instance for ambiguous names as all share a common concrete name.

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: AmbiguousQName -> Int

EmbPrj AmbiguousQName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: AmbiguousQName -> S Int32

icod_ :: AmbiguousQName -> S Int32

value :: Int32 -> R AmbiguousQName

NamesIn AmbiguousQName

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: AmbiguousQName -> Set QName

UniverseBi Declaration AmbiguousQName

Defined in Agda.Syntax.Abstract

Methods

universeBi :: Declaration -> [AmbiguousQName]

newtype 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

Fields

• mnameToList :: [Name]

Instances

Eq ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

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

(/=) :: ModuleName -> ModuleName -> Bool

Data ModuleName

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

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

toConstr :: ModuleName -> Constr

dataTypeOf :: ModuleName -> DataType

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

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

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

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

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

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

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

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

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

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

Ord ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: ModuleName -> ModuleName -> Ordering

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

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

(>) :: ModuleName -> ModuleName -> Bool

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

max :: ModuleName -> ModuleName -> ModuleName

min :: ModuleName -> ModuleName -> ModuleName

Show ModuleName

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

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> ModuleName -> ShowS

show :: ModuleName -> String

showList :: [ModuleName] -> ShowS

NFData ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: ModuleName -> ()

Pretty ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: ModuleName -> Doc

prettyPrec :: Int -> ModuleName -> Doc

prettyList :: [ModuleName] -> Doc

Sized ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

size :: ModuleName -> Int

KillRange ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT ModuleName

KillRange Sections

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Sections

SetRange ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> ModuleName -> ModuleName

HasRange ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: ModuleName -> Range

SubstExpr ModuleName

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName

ExprLike ModuleName

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> ModuleName -> m ModuleName

foldExpr :: Monoid m => (Expr -> m) -> ModuleName -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> ModuleName -> m ModuleName

mapExpr :: (Expr -> Expr) -> ModuleName -> ModuleName

EmbPrj ModuleName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ModuleName -> S Int32

icod_ :: ModuleName -> S Int32

value :: Int32 -> R ModuleName

PrettyTCM ModuleName

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: ModuleName -> TCM Doc

InstantiateFull ModuleName

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ModuleName -> ReduceM ModuleName

UniverseBi Declaration ModuleName

Defined in Agda.Syntax.Abstract

Methods

universeBi :: Declaration -> [ModuleName]

ToConcrete ModuleName QName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: ModuleName -> AbsToCon QName

bindToConcrete :: ModuleName -> (QName -> AbsToCon b) -> AbsToCon b

ToAbstract OldModuleName ModuleName

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: OldModuleName -> ScopeM ModuleName

ToAbstract NewModuleQName ModuleName

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: NewModuleQName -> ScopeM ModuleName

ToAbstract NewModuleName ModuleName

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: NewModuleName -> ScopeM ModuleName

ToAbstract ModuleAssignment (ModuleName, [LetBinding])

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: ModuleAssignment -> ScopeM (ModuleName, [LetBinding])

data QNamed a

Something preceeded by a qualified name.

Constructors

QNamed

Fields

• qname :: QName
• qnamed :: a

Instances

Functor QNamed

Defined in Agda.Syntax.Abstract.Name

Methods

fmap :: (a -> b) -> QNamed a -> QNamed b

(<$) :: a -> QNamed b -> QNamed a

Foldable QNamed

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

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

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

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

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

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

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

toList :: QNamed a -> [a]

null :: QNamed a -> Bool

length :: QNamed a -> Int

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

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

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

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

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

Traversable QNamed

Defined in Agda.Syntax.Abstract.Name

Methods

traverse :: Applicative f => (a -> f b) -> QNamed a -> f (QNamed b)

sequenceA :: Applicative f => QNamed (f a) -> f (QNamed a)

mapM :: Monad m => (a -> m b) -> QNamed a -> m (QNamed b)

sequence :: Monad m => QNamed (m a) -> m (QNamed a)

Show a => Show (QNamed a)

Use prettyShow to print names to the user.

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> QNamed a -> ShowS

show :: QNamed a -> String

showList :: [QNamed a] -> ShowS

Pretty a => Pretty (QNamed a)

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: QNamed a -> Doc

prettyPrec :: Int -> QNamed a -> Doc

prettyList :: [QNamed a] -> Doc

PrettyTCM (QNamed Clause)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: QNamed Clause -> TCM Doc

Reify (QNamed Clause) Clause

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: QNamed Clause0 -> TCM Clause

reifyWhen :: Bool -> QNamed Clause0 -> TCM Clause

ToAbstract (QNamed Clause) Clause

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: QNamed Clause0 -> WithNames Clause

ToAbstract [QNamed Clause] [Clause]

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: [QNamed Clause0] -> WithNames [Clause]

data 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

Fields

• qnameModule :: ModuleName
• qnameName :: Name

Instances

Eq QName

Defined in Agda.Syntax.Abstract.Name

Methods

(==) :: QName -> QName -> Bool

(/=) :: QName -> QName -> Bool

Data QName

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

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

toConstr :: QName -> Constr

dataTypeOf :: QName -> DataType

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

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

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

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

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

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

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

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

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

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

Ord QName

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: QName -> QName -> Ordering

(<) :: QName -> QName -> Bool

(<=) :: QName -> QName -> Bool

(>) :: QName -> QName -> Bool

(>=) :: QName -> QName -> Bool

max :: QName -> QName -> QName

min :: QName -> QName -> QName

Show QName

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

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> QName -> ShowS

show :: QName -> String

showList :: [QName] -> ShowS

NFData QName

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: QName -> ()

Hashable QName

Defined in Agda.Syntax.Abstract.Name

Methods

hashWithSalt :: Int -> QName -> Int

hash :: QName -> Int

Pretty QName

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: QName -> Doc

prettyPrec :: Int -> QName -> Doc

prettyList :: [QName] -> Doc

Sized QName

Defined in Agda.Syntax.Abstract.Name

Methods

size :: QName -> Int

KillRange QName

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT QName

KillRange RewriteRuleMap

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT RewriteRuleMap

KillRange Definitions

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Definitions

SetRange QName

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> QName -> QName

HasRange QName

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: QName -> Range

NumHoles QName

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: QName -> Int

TermLike QName

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> QName -> m QName

foldTerm :: Monoid m => (Term -> m) -> QName -> m

AllNames QName

Defined in Agda.Syntax.Abstract

Methods

allNames :: QName -> Seq QName

ExprLike QName

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> QName -> m QName

foldExpr :: Monoid m => (Expr -> m) -> QName -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> QName -> m QName

mapExpr :: (Expr -> Expr) -> QName -> QName

EmbPrj QName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QName -> S Int32

icod_ :: QName -> S Int32

value :: Int32 -> R QName

PrettyTCM QName

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: QName -> TCM Doc

NamesIn QName

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: QName -> Set QName

InstantiateFull QName

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: QName -> ReduceM QName

FromTerm QName

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction QName)

ToTerm QName

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (QName -> Term)

toTermR :: TCM (QName -> ReduceM Term)

PrimTerm QName

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: QName -> TCM Term

Occurs QName

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> QName -> TCM QName

metaOccurs :: MetaId -> QName -> TCM ()

Unquote QName

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM QName

UniverseBi Declaration QName

Defined in Agda.Syntax.Abstract

Methods

universeBi :: Declaration -> [QName]

Subst Term QName

Defined in Agda.TypeChecking.Substitute.Class

Methods

applySubst :: Substitution' Term -> QName -> QName

ToConcrete QName QName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: QName -> AbsToCon QName0

bindToConcrete :: QName -> (QName0 -> AbsToCon b) -> AbsToCon b

Conversion TOM Clause (Maybe ([Pat O], MExp O))

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O))

Conversion TOM Type (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O)

Conversion TOM Term (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O)

Conversion TOM Args (MM (ArgList O) (RefInfo O))

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O))

Conversion MOT (Exp O) Type

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type

Conversion MOT (Exp O) Term

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Term

Conversion TOM [Clause] [([Pat O], MExp O)]

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)]

Conversion TOM (Arg Pattern) (Pat O)

Defined in Agda.Auto.Convert

Methods

convert :: Arg Pattern -> TOM (Pat O)

Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b

Defined in Agda.Auto.Convert

Methods

convert :: MM a (RefInfo O) -> MOT b

(Show a, ToQName a) => ToAbstract (OldName a) QName

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: OldName a -> ScopeM QName

ToConcrete (Maybe QName) (Maybe Name)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Maybe QName -> AbsToCon (Maybe Name)

bindToConcrete :: Maybe QName -> (Maybe Name -> AbsToCon b) -> AbsToCon b

data 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

Fields

• nameId :: !NameId
• nameConcrete :: Name
• nameBindingSite :: Range
• nameFixity :: Fixity'

Instances

Eq Name

Defined in Agda.Syntax.Abstract.Name

Methods

(==) :: Name -> Name -> Bool

(/=) :: Name -> Name -> Bool

Data Name

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

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

toConstr :: Name -> Constr

dataTypeOf :: Name -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Name

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: Name -> Name -> Ordering

(<) :: Name -> Name -> Bool

(<=) :: Name -> Name -> Bool

(>) :: Name -> Name -> Bool

(>=) :: Name -> Name -> Bool

max :: Name -> Name -> Name

min :: Name -> Name -> Name

Show Name

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

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

NFData Name

The range is not forced.

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: Name -> ()

Hashable Name

Defined in Agda.Syntax.Abstract.Name

Methods

hashWithSalt :: Int -> Name -> Int

hash :: Name -> Int

Pretty Name

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: Name -> Doc

prettyPrec :: Int -> Name -> Doc

prettyList :: [Name] -> Doc

KillRange Name

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT Name

SetRange Name

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> Name -> Name

HasRange Name

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: Name -> Range

IsNoName Name

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

Defined in Agda.Syntax.Abstract.Name

Methods

isNoName :: Name -> Bool

NumHoles Name

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: Name -> Int

EmbPrj Name

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32

icod_ :: Name -> S Int32

value :: Int32 -> R Name

PrettyTCM Name

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Name -> TCM Doc

AddContext Name

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Name -> tcm a -> tcm a

contextSize :: Name -> Nat

InstantiateFull Name

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Name -> ReduceM Name

Subst Term Name

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' Term -> Name -> Name

ToConcrete Name Name

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Name -> AbsToCon Name0

bindToConcrete :: Name -> (Name0 -> AbsToCon b) -> AbsToCon b

Reify Name Name

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Name -> TCM Name

reifyWhen :: Bool -> Name -> TCM Name

Suggest Name (Abs b)

Defined in Agda.Syntax.Internal

Methods

suggest :: Name -> Abs b -> String

ToAbstract Pattern (Names, Pattern)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: Pattern0 -> WithNames (Names, Pattern)

AddContext (Dom (Name, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (Name, Type) -> tcm a -> tcm a

contextSize :: Dom (Name, Type) -> Nat

ToAbstract (NewName Name) Name

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: NewName Name0 -> ScopeM Name

ToAbstract (NewName BoundName) Name

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: NewName BoundName -> ScopeM Name

(Free i, Reify i a) => Reify (Abs i) (Name, a)

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Abs i -> TCM (Name, a)

reifyWhen :: Bool -> Abs i -> TCM (Name, a)

ToAbstract r a => ToAbstract (Abs r) (a, Name)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: Abs r -> WithNames (a, Name)

AddContext ([WithHiding Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([WithHiding Name], Dom Type) -> tcm a -> tcm a

contextSize :: ([WithHiding Name], Dom Type) -> Nat

AddContext ([Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Name], Dom Type) -> tcm a -> tcm a

contextSize :: ([Name], Dom Type) -> Nat

AddContext (Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => (Name, Dom Type) -> tcm a -> tcm a

contextSize :: (Name, Dom Type) -> Nat

ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBindings

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: (Dom r, Name) -> WithNames TypedBindings

unambiguous :: QName -> AmbiguousQName

A singleton "ambiguous" name.

headAmbQ :: AmbiguousQName -> QName

Get the first of the ambiguous names.

isAmbiguous :: AmbiguousQName -> Bool

Is a name ambiguous.

getUnambiguous :: AmbiguousQName -> Maybe QName

Get the name if unambiguous.

isAnonymousModuleName :: ModuleName -> Bool

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

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

withRangesOfQ :: ModuleName -> QName -> ModuleName

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

mnameFromList :: [Name] -> ModuleName

noModuleName :: ModuleName

commonParentModule :: ModuleName -> ModuleName -> ModuleName

qnameToList :: QName -> [Name]

qnameFromList :: [Name] -> QName

qnameToMName :: QName -> ModuleName

mnameToQName :: ModuleName -> QName

showQNameId :: QName -> String

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

mnameToConcrete :: ModuleName -> QName

toTopLevelModuleName :: ModuleName -> TopLevelModuleName

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

qualifyQ :: ModuleName -> QName -> QName

qualify :: ModuleName -> Name -> QName

qualify_ :: Name -> QName

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

isOperator :: QName -> Bool

Is the name an operator?

isSubModuleOf :: ModuleName -> ModuleName -> Bool

isInModule :: QName -> ModuleName -> Bool

nextName :: Name -> Name

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

class IsNoName a where

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

Minimal complete definition

isNoName

Methods

isNoName :: a -> Bool

Instances

IsNoName String

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: String -> Bool

IsNoName ByteString

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: ByteString -> Bool

IsNoName QName

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: QName -> Bool

IsNoName Name

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Name -> Bool

IsNoName Name

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

Defined in Agda.Syntax.Abstract.Name

Methods

isNoName :: Name -> Bool