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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Abstract.Name

Description

Abstract names carry unique identifiers and stuff.

Synopsis

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
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
IsProjP Void Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

IsProjP Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

IsProjP (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

IsProjP a => IsProjP (Named n a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) 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 
Instances
Eq AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

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

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 Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Show AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> AmbiguousQName -> ShowS

show :: AmbiguousQName -> String

showList :: [AmbiguousQName] -> ShowS

Pretty AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

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

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 #

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 #

NamesIn AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

UniverseBi Declaration AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Instances
Eq ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

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

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 Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Show ModuleName Source #

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

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> ModuleName -> ShowS

show :: ModuleName -> String

showList :: [ModuleName] -> ShowS

NFData ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: ModuleName -> ()

Pretty ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Sized ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

size :: ModuleName -> Int Source #

KillRange ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange Sections Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

SetRange ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

HasRange ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

SubstExpr ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

mapExpr :: (Expr -> Expr) -> ModuleName -> 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 #

PrettyTCM ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

InstantiateFull ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

UniverseBi Declaration ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete ModuleName QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract OldModuleName ModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract NewModuleQName ModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract NewModuleName ModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract ModuleAssignment (ModuleName, [LetBinding]) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data QNamed a Source #

Something preceeded by a qualified name.

Constructors

QNamed 

Fields

Instances
Functor QNamed Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

Foldable QNamed Source # 
Instance details

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 Source # 
Instance details

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) Source #

Use prettyShow to print names to the user.

Instance details

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

PrettyTCM (QNamed Clause) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

ToAbstract (QNamed Clause) Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Reify (QNamed Clause) Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

ToAbstract [QNamed Clause] [Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Reify (QNamed System) [Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

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 
Instances
Eq QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

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

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 Source # 
Instance details

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 Source #

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

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> QName -> ShowS

show :: QName -> String

showList :: [QName] -> ShowS

NFData QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: QName -> ()

Hashable QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

hashWithSalt :: Int -> QName -> Int

hash :: QName -> Int

Pretty QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Sized QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

size :: QName -> Int Source #

KillRange QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange RewriteRuleMap Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Definitions Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

SetRange QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> QName -> QName Source #

HasRange QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: QName -> Range Source #

LensInScope QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

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 #

AllNames QName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

allNames :: QName -> Seq QName Source #

ExprLike QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

mapExpr :: (Expr -> Expr) -> QName -> 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 #

PrettyTCM QName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: QName -> TCM Doc Source #

NamesIn QName Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: QName -> Set QName Source #

InstantiateFull QName Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Occurs QName Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

FromTerm QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: QName -> TCM Term Source #

Unquote QName Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

UniverseBi Declaration QName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Subst Term QName Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.Class

ToConcrete QName QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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 Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (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 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) Type Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type Source #

Conversion MOT (Exp O) Term Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Term 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 TOM (Arg Pattern) (Pat O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Arg Pattern -> TOM (Pat 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 #

(Show a, ToQName a) => ToAbstract (OldName a) QName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToConcrete (Maybe QName) (Maybe Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

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

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

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.

Instances
Eq Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

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

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 Source # 
Instance details

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 Source #

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

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

NFData Name Source #

The range is not forced.

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: Name -> ()

Hashable Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

hashWithSalt :: Int -> Name -> Int

hash :: Name -> Int

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 #

KillRange Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

SetRange Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> Name -> Name Source #

HasRange Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: Name -> Range 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

NumHoles Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: Name -> Int 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 #

PrettyTCM Name Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Name -> TCM Doc Source #

AddContext Name Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Name -> Nat Source #

InstantiateFull Name Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst Term Name Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

ToConcrete Name Name Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Reify Name Name Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Name -> TCM Name Source #

reifyWhen :: Bool -> Name -> TCM Name Source #

Suggest Name (Abs b) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

suggest :: Name -> Abs b -> String Source #

ToAbstract Pattern (Names, Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

AddContext (Dom (Name, Type)) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

ToAbstract (NewName Name) Name Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract r a => ToAbstract (Abs r) (a, Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

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

(Free i, Reify i a) => Reify (Abs i) (Name, a) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

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

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

AddContext ([NamedArg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: ([NamedArg Name], Type) -> Nat Source #

AddContext ([Arg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: ([Arg Name], Type) -> Nat Source #

AddContext ([WithHiding Name], Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([Name], Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Name, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

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.

toTopLevelModuleName :: ModuleName -> TopLevelModuleName Source #

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

Precondition: The module name must be well-formed.

qualify_ :: Name -> QName Source #

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

isOperator :: QName -> Bool Source #

Is the name an operator?

nextName :: Name -> Name Source #

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

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

class IsNoName a where Source #

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

Methods

isNoName :: a -> Bool Source #

Instances
IsNoName String Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: String -> Bool Source #

IsNoName ByteString Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: ByteString -> Bool Source #

IsNoName QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: QName -> Bool Source #

IsNoName Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Name -> Bool 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 #