Agda-2.6.2.2: 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

Instances details
MkName String Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

class IsProjP a where Source #

Check whether we are a projection pattern.

Instances

Instances details
IsProjP Void Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

IsProjP Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

IsProjP a => IsProjP (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

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

data Suffix Source #

A name suffix

Constructors

NoSuffix 
Suffix !Integer 

Instances

Instances details
Eq Suffix Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

(==) :: Suffix -> Suffix -> Bool #

(/=) :: Suffix -> Suffix -> Bool #

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 #

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

toConstr :: Suffix -> Constr #

dataTypeOf :: Suffix -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Suffix Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Show Suffix Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

NFData Suffix Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: Suffix -> () #

Pretty Suffix Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

KillRange Suffix Source # 
Instance details

Defined in Agda.Syntax.Abstract

EmbPrj Suffix Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

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

Instances

Instances details
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 :: forall r r'. (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

NFData AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: AmbiguousQName -> () #

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

EmbPrj AmbiguousQName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

NamesIn AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> AmbiguousQName -> m 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

Instances

Instances details
Eq ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

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 :: forall r r'. (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 # 
Instance details

Defined in Agda.Syntax.Abstract.Name

NFData ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: ModuleName -> () #

Sized ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

size :: ModuleName -> Int Source #

Pretty ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

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

SetBindingSite ModuleName Source #

Sets the binding site of all names in the path.

Instance details

Defined in Agda.Syntax.Scope.Base

SubstExpr ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

EmbPrj ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

PrettyTCM ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

ToConcrete ModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleName Source #

InstantiateFull ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

type ConOfAbs ModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

data QNamed a Source #

Something preceeded by a qualified name.

Constructors

QNamed 

Fields

Instances

Instances details
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 #

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

PrettyTCM (QNamed Clause) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

ToAbstract [QNamed Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

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

ToAbstract (QNamed Clause) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (QNamed Clause) Source #

Reify (QNamed Clause) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (QNamed Clause) Source #

Reify (QNamed System) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (QNamed System) Source #

type AbsOfRef [QNamed Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (List1 (QNamed Clause)) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (QNamed Clause) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type ReifiesTo (QNamed Clause) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (QNamed System) 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

Instances details
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 :: forall r r'. (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 # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> QName -> ShowS #

show :: QName -> String #

showList :: [QName] -> ShowS #

Hashable QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

hashWithSalt :: Int -> QName -> Int #

hash :: QName -> Int #

NFData QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: QName -> () #

Sized QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

size :: QName -> Int Source #

Pretty QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

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 #

LensFixity' QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

LensFixity QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

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 #

SetBindingSite QName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Subst QName Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.Class

Associated Types

type SubstArg QName 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 #

DeclaredNames RecordDirectives Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

DeclaredNames KName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

EmbPrj QName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

PrettyTCM QName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => QName -> m Doc Source #

NamesIn QName Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> QName -> m Source #

ToConcrete QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs QName Source #

InstantiateFull QName Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

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 #

PrimType QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primType :: QName -> TCM Type Source #

Occurs QName Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Unquote QName Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

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 #

ToConcrete (Maybe QName) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe QName) Source #

type SubstArg QName Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.Class

type ConOfAbs QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe QName) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Instances

Instances details
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 :: forall r r'. (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 #

Use prettyShow to print names to the user.

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> Name -> ShowS #

show :: Name -> String #

showList :: [Name] -> ShowS #

Hashable Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

hashWithSalt :: Int -> Name -> Int #

hash :: Name -> Int #

NFData Name Source #

The range is not forced.

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: Name -> () #

Pretty Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

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 #

LensFixity' Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

LensFixity Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

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 #

SetBindingSite Name Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Suggest Name Source # 
Instance details

Defined in Agda.Syntax.Internal

Subst Name Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Name Source #

EmbPrj Name Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

PrettyTCM Name Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Name -> m Doc 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 #

ToConcrete Name Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Name Source #

InstantiateFull Name Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reify Name Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Name Source #

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

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Dom (Name, Type) -> m Doc 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 #

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 ([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 ([WithHiding Name], Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

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 (NamedArg Name), Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

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 (WithHiding Name), Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Monad.Context

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 #

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

type SubstArg Name Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type ConOfAbs Name Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ReifiesTo Name Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type AbsOfRef (Dom r, Name) 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 -> 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.

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?

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?

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.

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

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 #

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

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