Agda
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Abstract.Name

Description

Abstract names carry unique identifiers and stuff.

Synopsis

Documentation

ambAbstractNames :: AmbiguousQName -> [AbstractName] Source #

ambigName :: List1 AbstractName -> AmbiguousQName Source #

ambiguous :: List1 QName -> AmbiguousQName Source #

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

fromAmbQName :: AmbQNameEntry -> QName Source #

generalizedVarsMetadata :: Map QName Name -> NameMetadata Source #

getAmbiguous :: AmbiguousQName -> List1 QName Source #

getUnambiguous :: AmbiguousQName -> Maybe QName Source #

Get the name if unambiguous.

headAmbQ :: AmbiguousQName -> QName Source #

Get the first of the ambiguous names.

instanceMetadata :: IsInstance -> NameMetadata Source #

isAmbiguous :: AmbiguousQName -> Bool Source #

Is a name ambiguous.

isAnonymousModuleName :: ModuleName -> Bool Source #

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

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

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

Is the first module a weak child of the second?

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

Is the first module a weak parent of the second?

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

Is the first module a proper child of the second?

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

Is the first module a proper parent of the second?

isOperator :: QName -> Bool Source #

Is the name an operator?

lensAmodName :: Lens' AbstractModule ModuleName Source #

Van Laarhoven lens on amodName.

lensAnameName :: Lens' AbstractName QName Source #

Van Laarhoven lens on anameName.

lensQNameName :: Lens' QName Name Source #

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

mergeAmbQ :: AmbiguousQName -> AmbiguousQName -> AmbiguousQName Source #

Preserve lineage information from both maps, left-biased.

mnameFromList :: [Name] -> ModuleName Source #

mnameFromList1 :: List1 Name -> ModuleName Source #

mnameToConcrete :: ModuleName -> QName Source #

mnameToList1 :: ModuleName -> List1 Name Source #

mnameToQName :: ModuleName -> QName Source #

nameToArgName :: Name -> ArgName Source #

namedArgName :: NamedArg Name -> ArgName 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.

noMetadata :: NameMetadata Source #

noModuleName :: ModuleName Source #

qnameFromList :: List1 Name -> QName 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.

qnameToList :: QName -> List1 Name Source #

qnameToList0 :: QName -> [Name] Source #

qnameToMName :: QName -> ModuleName Source #

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

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

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

qualify_ :: Name -> QName Source #

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

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

Ignoring the suffix.

showQNameId :: QName -> String Source #

uglyShowName :: Name -> String Source #

Useful for debugging scoping problems

unambigName :: AbstractName -> AmbiguousQName Source #

unambiguous :: QName -> AmbiguousQName Source #

A singleton "ambiguous" name.

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.

data AbstractModule Source #

A decoration of abstract syntax module names.

Constructors

AbsModule 

Fields

Instances

Instances details
HasNameBindingSite AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

nameBindingSite :: AbstractModule -> Range Source #

Pretty AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: AbstractModule -> Doc Source #

prettyPrec :: Int -> AbstractModule -> Doc Source #

prettyList :: [AbstractModule] -> Doc Source #

InScope AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

inScopeTag :: InScopeTag AbstractModule Source #

SetBindingSite AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> AbstractModule -> AbstractModule Source #

EmbPrj AbstractModule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractModule -> S Word32 Source #

icod_ :: AbstractModule -> S Word32 Source #

value :: Word32 -> R AbstractModule Source #

NFData AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: AbstractModule -> () #

Generic AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Associated Types

type Rep AbstractModule 
Instance details

Defined in Agda.Syntax.Abstract.Name

type Rep AbstractModule = D1 ('MetaData "AbstractModule" "Agda.Syntax.Abstract.Name" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "AbsModule" 'PrefixI 'True) (S1 ('MetaSel ('Just "amodName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Just "amodLineage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope)))

Methods

from :: AbstractModule -> Rep AbstractModule x #

to :: Rep AbstractModule x -> AbstractModule #

Show AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> AbstractModule -> ShowS #

show :: AbstractModule -> String #

showList :: [AbstractModule] -> ShowS #

Eq AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

Ord AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: AbstractModule -> AbstractModule -> Ordering #

(<) :: AbstractModule -> AbstractModule -> Bool #

(<=) :: AbstractModule -> AbstractModule -> Bool #

(>) :: AbstractModule -> AbstractModule -> Bool #

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

max :: AbstractModule -> AbstractModule -> AbstractModule #

min :: AbstractModule -> AbstractModule -> AbstractModule #

type Rep AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

type Rep AbstractModule = D1 ('MetaData "AbstractModule" "Agda.Syntax.Abstract.Name" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "AbsModule" 'PrefixI 'True) (S1 ('MetaSel ('Just "amodName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Just "amodLineage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope)))

data AbstractName Source #

A decoration of QName.

Constructors

AbsName 

Fields

Instances

Instances details
NameToExpr AbstractName Source #

Turn an AbstractName into an expression.

Instance details

Defined in Agda.Syntax.Abstract

Methods

nameToExpr :: AbstractName -> Expr Source #

HasNameBindingSite AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

nameBindingSite :: AbstractName -> Range Source #

HasNameId AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

nameId :: AbstractName -> NameId Source #

IsInstanceDef AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

isInstanceDef :: AbstractName -> Maybe KwRange Source #

LensFixity AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

lensFixity :: Lens' AbstractName Fixity Source #

Pretty AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: AbstractName -> Doc Source #

prettyPrec :: Int -> AbstractName -> Doc Source #

prettyList :: [AbstractName] -> Doc Source #

HasRange AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: AbstractName -> Range Source #

KillRange AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT AbstractName Source #

SetRange AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> AbstractName -> AbstractName Source #

InScope AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

inScopeTag :: InScopeTag AbstractName Source #

SetBindingSite AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> AbstractName -> AbstractName Source #

ToConcrete AbstractName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs AbstractName 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs AbstractName = QName

Methods

toConcrete :: MonadToConcrete m => AbstractName -> m (ConOfAbs AbstractName) Source #

bindToConcrete :: MonadToConcrete m => AbstractName -> (ConOfAbs AbstractName -> m b) -> m b Source #

PrettyTCM AbstractName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

EmbPrj AbstractName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractName -> S Word32 Source #

icod_ :: AbstractName -> S Word32 Source #

value :: Word32 -> R AbstractName Source #

NFData AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: AbstractName -> () #

Generic AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Associated Types

type Rep AbstractName 
Instance details

Defined in Agda.Syntax.Abstract.Name

type Rep AbstractName = D1 ('MetaData "AbstractName" "Agda.Syntax.Abstract.Name" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "AbsName" 'PrefixI 'True) ((S1 ('MetaSel ('Just "anameName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "anameKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName)) :*: (S1 ('MetaSel ('Just "anameLineage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope) :*: S1 ('MetaSel ('Just "anameMetadata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameMetadata))))

Methods

from :: AbstractName -> Rep AbstractName x #

to :: Rep AbstractName x -> AbstractName #

Show AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> AbstractName -> ShowS #

show :: AbstractName -> String #

showList :: [AbstractName] -> ShowS #

Eq AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

Ord AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: AbstractName -> AbstractName -> Ordering #

(<) :: AbstractName -> AbstractName -> Bool #

(<=) :: AbstractName -> AbstractName -> Bool #

(>) :: AbstractName -> AbstractName -> Bool #

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

max :: AbstractName -> AbstractName -> AbstractName #

min :: AbstractName -> AbstractName -> AbstractName #

Hashable AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

hashWithSalt :: Int -> AbstractName -> Int #

hash :: AbstractName -> Int #

type ConOfAbs AbstractName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs AbstractName = QName
type Rep AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

type Rep AbstractName = D1 ('MetaData "AbstractName" "Agda.Syntax.Abstract.Name" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "AbsName" 'PrefixI 'True) ((S1 ('MetaSel ('Just "anameName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "anameKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName)) :*: (S1 ('MetaSel ('Just "anameLineage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope) :*: S1 ('MetaSel ('Just "anameMetadata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameMetadata))))

data AmbQNameEntry Source #

Alternative in AmbiguousQName.

Constructors

AmbQName QName

QName without lineage information.

AmbAbstractName AbstractName

QName with lineage information, for error reporting.

Instances

Instances details
HasRange AmbQNameEntry Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: AmbQNameEntry -> Range Source #

KillRange AmbQNameEntry Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT AmbQNameEntry Source #

NFData AmbQNameEntry Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: AmbQNameEntry -> () #

Semigroup AmbQNameEntry Source #

Prefer AmbAbstractName over AmbQName, left-biased.

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

(<>) :: AmbQNameEntry -> AmbQNameEntry -> AmbQNameEntry #

sconcat :: NonEmpty AmbQNameEntry -> AmbQNameEntry #

stimes :: Integral b => b -> AmbQNameEntry -> AmbQNameEntry #

Generic AmbQNameEntry Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Associated Types

type Rep AmbQNameEntry 
Instance details

Defined in Agda.Syntax.Abstract.Name

type Rep AmbQNameEntry = D1 ('MetaData "AmbQNameEntry" "Agda.Syntax.Abstract.Name" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "AmbQName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "AmbAbstractName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AbstractName)))

Methods

from :: AmbQNameEntry -> Rep AmbQNameEntry x #

to :: Rep AmbQNameEntry x -> AmbQNameEntry #

Show AmbQNameEntry Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> AmbQNameEntry -> ShowS #

show :: AmbQNameEntry -> String #

showList :: [AmbQNameEntry] -> ShowS #

Eq AmbQNameEntry Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

Ord AmbQNameEntry Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: AmbQNameEntry -> AmbQNameEntry -> Ordering #

(<) :: AmbQNameEntry -> AmbQNameEntry -> Bool #

(<=) :: AmbQNameEntry -> AmbQNameEntry -> Bool #

(>) :: AmbQNameEntry -> AmbQNameEntry -> Bool #

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

max :: AmbQNameEntry -> AmbQNameEntry -> AmbQNameEntry #

min :: AmbQNameEntry -> AmbQNameEntry -> AmbQNameEntry #

type Rep AmbQNameEntry Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

type Rep AmbQNameEntry = D1 ('MetaData "AmbQNameEntry" "Agda.Syntax.Abstract.Name" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "AmbQName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "AmbAbstractName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AbstractName)))

newtype AmbiguousQName Source #

Ambiguous qualified names. Used for overloaded constructors.

A QName in this collection might be equipped with lineage information in form of an associated AbstractName (which must contain the same QName).

Invariant: All the names in the map must have the same concrete, unqualified name. (This implies that they all have the same Range).

Don't use the constructor AmbQ directly, use the smart constructors below!

Constructors

AmbQ 

Fields

Instances

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

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

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> 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 #

Note: Serialization of AmbiguousQName discards lineage, treating all entries as just QName rather than AbstractName.

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: AmbiguousQName -> S Word32 Source #

icod_ :: AmbiguousQName -> S Word32 Source #

value :: Word32 -> R AmbiguousQName Source #

Sized AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

size :: AmbiguousQName -> Int Source #

natSize :: AmbiguousQName -> Peano Source #

NFData AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: AmbiguousQName -> () #

Show AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> AmbiguousQName -> ShowS #

show :: AmbiguousQName -> String #

showList :: [AmbiguousQName] -> ShowS #

Eq AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

Ord AmbiguousQName Source # 
Instance details

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 #

class HasNameBindingSite a where Source #

Methods

nameBindingSite :: a -> Range Source #

Instances

Instances details
HasNameBindingSite AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

nameBindingSite :: AbstractModule -> Range Source #

HasNameBindingSite AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

nameBindingSite :: AbstractName -> Range Source #

HasNameBindingSite ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

nameBindingSite :: ModuleName -> Range Source #

HasNameBindingSite Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

nameBindingSite :: Name -> Range Source #

HasNameBindingSite QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

nameBindingSite :: QName -> Range Source #

class HasNameId a where Source #

Methods

nameId :: a -> NameId Source #

Instances

Instances details
HasNameId AbstractName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

nameId :: AbstractName -> NameId Source #

HasNameId Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

nameId :: Name -> NameId Source #

HasNameId QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

nameId :: QName -> NameId 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 KindOfName Source #

For the sake of parsing left-hand sides, we distinguish constructor and record field names from defined names.

Constructors

ConName

Constructor name (Inductive or don't know).

CoConName

Constructor name (definitely CoInductive).

FldName

Record field name.

PatternSynName

Name of a pattern synonym.

GeneralizeName

Name to be generalized

DisallowedGeneralizeName

Generalizable variable from a let open

MacroName

Name of a macro

QuotableName

A name that can only be quoted. Previous category DefName: (Refined in a flat manner as Enum and Bounded are not hereditary.)

DataName

Name of a data.

RecName

Name of a record.

FunName

Name of a defined function.

AxiomName

Name of a postulate.

PrimName

Name of a primitive.

OtherDefName

A DefName, but either other kind or don't know which kind. End DefName. Keep these together in sequence, for sake of isDefName!

Instances

Instances details
KillRange KindOfName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT KindOfName Source #

EmbPrj KindOfName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: KindOfName -> S Word32 Source #

icod_ :: KindOfName -> S Word32 Source #

value :: Word32 -> R KindOfName Source #

NFData KindOfName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: KindOfName -> () #

Bounded KindOfName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

minBound :: KindOfName #

maxBound :: KindOfName #

Enum KindOfName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

succ :: KindOfName -> KindOfName #

pred :: KindOfName -> KindOfName #

toEnum :: Int -> KindOfName #

fromEnum :: KindOfName -> Int #

enumFrom :: KindOfName -> [KindOfName] #

enumFromThen :: KindOfName -> KindOfName -> [KindOfName] #

enumFromTo :: KindOfName -> KindOfName -> [KindOfName] #

enumFromThenTo :: KindOfName -> KindOfName -> KindOfName -> [KindOfName] #

Generic KindOfName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Associated Types

type Rep KindOfName 
Instance details

Defined in Agda.Syntax.Abstract.Name

type Rep KindOfName = D1 ('MetaData "KindOfName" "Agda.Syntax.Abstract.Name" "Agda-2.9.0-inplace" 'False) (((C1 ('MetaCons "ConName" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CoConName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FldName" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PatternSynName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GeneralizeName" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DisallowedGeneralizeName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MacroName" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "QuotableName" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DataName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RecName" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "FunName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AxiomName" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OtherDefName" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: KindOfName -> Rep KindOfName x #

to :: Rep KindOfName x -> KindOfName #

Show KindOfName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> KindOfName -> ShowS #

show :: KindOfName -> String #

showList :: [KindOfName] -> ShowS #

Eq KindOfName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

Ord KindOfName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: KindOfName -> KindOfName -> Ordering #

(<) :: KindOfName -> KindOfName -> Bool #

(<=) :: KindOfName -> KindOfName -> Bool #

(>) :: KindOfName -> KindOfName -> Bool #

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

max :: KindOfName -> KindOfName -> KindOfName #

min :: KindOfName -> KindOfName -> KindOfName #

type Rep KindOfName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

type Rep KindOfName = D1 ('MetaData "KindOfName" "Agda.Syntax.Abstract.Name" "Agda-2.9.0-inplace" 'False) (((C1 ('MetaCons "ConName" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CoConName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FldName" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PatternSynName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GeneralizeName" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DisallowedGeneralizeName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MacroName" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "QuotableName" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DataName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RecName" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "FunName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AxiomName" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OtherDefName" 'PrefixI 'False) (U1 :: Type -> Type)))))

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 #

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

Defined in Agda.Syntax.Abstract

Methods

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

HasNameBindingSite ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

nameBindingSite :: ModuleName -> Range 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 #

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 #

IsNoName ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

isNoName :: ModuleName -> Bool 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 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs ModuleName = QName

Methods

toConcrete :: MonadToConcrete m => ModuleName -> m (ConOfAbs ModuleName) Source #

bindToConcrete :: MonadToConcrete m => ModuleName -> (ConOfAbs ModuleName -> m b) -> m 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 Word32 Source #

icod_ :: ModuleName -> S Word32 Source #

value :: Word32 -> R ModuleName Source #

Null ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

empty :: ModuleName Source #

null :: ModuleName -> Bool Source #

Sized ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

size :: ModuleName -> Int Source #

natSize :: ModuleName -> Peano Source #

NFData ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: ModuleName -> () #

Show ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> ModuleName -> ShowS #

show :: ModuleName -> String #

showList :: [ModuleName] -> ShowS #

Eq ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

Ord ModuleName Source # 
Instance details

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 #

Hashable ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

hashWithSalt :: Int -> ModuleName -> Int #

hash :: ModuleName -> Int #

type ConOfAbs ModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs ModuleName = QName

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

Defined in Agda.Syntax.Abstract.Name

Methods

nameBindingSite :: Name -> Range Source #

HasNameId Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

nameId :: Name -> NameId Source #

LensFixity Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

lensFixity :: Lens' Name Fixity Source #

LensFixity' Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

lensFixity' :: Lens' Name Fixity' 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 #

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' Name NameInScope 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 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs Name = Name

Methods

toConcrete :: MonadToConcrete m => Name -> m (ConOfAbs Name) Source #

bindToConcrete :: MonadToConcrete m => Name -> (ConOfAbs Name -> m b) -> m b Source #

Reify Name Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Name 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Name = Name

Methods

reify :: MonadReify m => Name -> m (ReifiesTo Name) Source #

reifyWhen :: MonadReify m => Bool -> Name -> m (ReifiesTo Name) Source #

FreshName Name Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freshName_ :: MonadFresh NameId m => Name -> m 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 Word32 Source #

icod_ :: Name -> S Word32 Source #

value :: Word32 -> R Name Source #

Subst Name Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Name 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg Name = Term

Methods

applySubst :: Substitution' (SubstArg Name) -> Name -> Name Source #

Null Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

empty :: Name Source #

null :: Name -> Bool Source #

NFData Name Source #

The range is not forced.

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: Name -> () #

Show Name Source #

Show instances (only for debug printing!)

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 #

Eq Name Source #

Important instances: Eq, Ord, Hashable

For the identity and comparing of names, only the NameId matters!

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

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 #

Hashable Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

hashWithSalt :: Int -> Name -> Int #

hash :: Name -> Int #

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 #

(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) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Dom r, Name) = TypedBinding

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (List1 (Dom Name), Type) -> m a -> m a Source #

contextSize :: (List1 (Dom Name), 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 #

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 #

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

data NameMetadata Source #

Constructors

NameMetadata 

Fields

Instances

Instances details
IsInstanceDef NameMetadata Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

isInstanceDef :: NameMetadata -> Maybe KwRange Source #

KillRange NameMetadata Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT NameMetadata Source #

EmbPrj NameMetadata Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameMetadata -> S Word32 Source #

icod_ :: NameMetadata -> S Word32 Source #

value :: Word32 -> R NameMetadata Source #

Null NameMetadata Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

empty :: NameMetadata Source #

null :: NameMetadata -> Bool Source #

NFData NameMetadata Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: NameMetadata -> () #

Generic NameMetadata Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Associated Types

type Rep NameMetadata 
Instance details

Defined in Agda.Syntax.Abstract.Name

type Rep NameMetadata = D1 ('MetaData "NameMetadata" "Agda.Syntax.Abstract.Name" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "NameMetadata" 'PrefixI 'True) (S1 ('MetaSel ('Just "nameDataGeneralizedVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName Name)) :*: S1 ('MetaSel ('Just "nameDataIsInstance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance)))

Methods

from :: NameMetadata -> Rep NameMetadata x #

to :: Rep NameMetadata x -> NameMetadata #

Show NameMetadata Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> NameMetadata -> ShowS #

show :: NameMetadata -> String #

showList :: [NameMetadata] -> ShowS #

type Rep NameMetadata Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

type Rep NameMetadata = D1 ('MetaData "NameMetadata" "Agda.Syntax.Abstract.Name" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "NameMetadata" 'PrefixI 'True) (S1 ('MetaSel ('Just "nameDataGeneralizedVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName Name)) :*: S1 ('MetaSel ('Just "nameDataIsInstance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance)))

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

Instances

Instances details
HasNameBindingSite QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

nameBindingSite :: QName -> Range Source #

HasNameId QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

nameId :: QName -> NameId 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' QName Fixity Source #

LensFixity' QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

lensFixity' :: Lens' QName Fixity' 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 #

LensInScope QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

lensInScope :: Lens' QName NameInScope 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

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> 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 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs QName = QName

Methods

toConcrete :: MonadToConcrete m => QName -> m (ConOfAbs QName) Source #

bindToConcrete :: MonadToConcrete m => QName -> (ConOfAbs QName -> m b) -> m b Source #

Occurs QName Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: QName -> OccursM QName Source #

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

ChaseDisplayForms QName Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Signature

Methods

chaseDisplayForms :: QName -> Set QName -> TCM (Set QName) Source #

PrettyTCM QName Source #

Automatically highlights the resulting document with the correct name kind.

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

icod_ :: QName -> S Word32 Source #

value :: Word32 -> R QName Source #

Subst QName Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.Class

Associated Types

type SubstArg QName 
Instance details

Defined in Agda.TypeChecking.Substitute.Class

type SubstArg QName = Term

Methods

applySubst :: Substitution' (SubstArg QName) -> QName -> QName Source #

Unquote QName Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM QName Source #

Null QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

empty :: QName Source #

null :: QName -> Bool Source #

Sized QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

size :: QName -> Int Source #

natSize :: QName -> Peano Source #

NFData QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: QName -> () #

Generic QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Associated Types

type Rep QName 
Instance details

Defined in Agda.Syntax.Abstract.Name

type Rep QName = D1 ('MetaData "QName" "Agda.Syntax.Abstract.Name" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "QName" 'PrefixI 'True) (S1 ('MetaSel ('Just "qnameModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Just "qnameName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)))

Methods

from :: QName -> Rep QName x #

to :: Rep QName x -> QName #

Show QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> QName -> ShowS #

show :: QName -> String #

showList :: [QName] -> ShowS #

Eq QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

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 #

Hashable QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

hashWithSalt :: Int -> QName -> Int #

hash :: QName -> Int #

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

Defined in Agda.Syntax.Abstract.Name

type Rep QName = D1 ('MetaData "QName" "Agda.Syntax.Abstract.Name" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "QName" 'PrefixI 'True) (S1 ('MetaSel ('Just "qnameModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Just "qnameName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)))

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

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 #

Reify (QNamed Clause) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (QNamed Clause) 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (QNamed Clause) = Clause

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) 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (QNamed System) = [Clause]

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) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (QNamed Clause) = Clause

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)) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (List1 (QNamed Clause)) = List1 Clause

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] 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef [QNamed Clause] = [Clause]

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 #

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 #

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

A name suffix.

Constructors

NoSuffix 
Suffix !Integer 

Instances

Instances details
Pretty Suffix Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: Suffix -> Doc Source #

prettyPrec :: Int -> Suffix -> Doc Source #

prettyList :: [Suffix] -> Doc Source #

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

icod_ :: Suffix -> S Word32 Source #

value :: Word32 -> R Suffix Source #

Null Suffix Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

empty :: Suffix Source #

null :: Suffix -> Bool Source #

NFData Suffix Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: Suffix -> () #

Show Suffix Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> Suffix -> ShowS #

show :: Suffix -> String #

showList :: [Suffix] -> ShowS #

Eq Suffix Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

Ord Suffix Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: Suffix -> Suffix -> Ordering #

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

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

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

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

max :: Suffix -> Suffix -> Suffix #

min :: Suffix -> Suffix -> Suffix #

data WhyInScope Source #

Where does a name come from?

This information is solely for reporting to the user, see whyInScope.

Constructors

Defined

Defined in this module.

Opened QName WhyInScope

Imported from another module.

Applied QName WhyInScope

Imported by a module application.

Instances

Instances details
KillRange WhyInScope Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT WhyInScope Source #

EmbPrj WhyInScope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: WhyInScope -> S Word32 Source #

icod_ :: WhyInScope -> S Word32 Source #

value :: Word32 -> R WhyInScope Source #

NFData WhyInScope Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: WhyInScope -> () #

Generic WhyInScope Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Associated Types

type Rep WhyInScope 
Instance details

Defined in Agda.Syntax.Abstract.Name

type Rep WhyInScope = D1 ('MetaData "WhyInScope" "Agda.Syntax.Abstract.Name" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "Defined" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Opened" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope)) :+: C1 ('MetaCons "Applied" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope))))

Methods

from :: WhyInScope -> Rep WhyInScope x #

to :: Rep WhyInScope x -> WhyInScope #

Show WhyInScope Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> WhyInScope -> ShowS #

show :: WhyInScope -> String #

showList :: [WhyInScope] -> ShowS #

type Rep WhyInScope Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

type Rep WhyInScope = D1 ('MetaData "WhyInScope" "Agda.Syntax.Abstract.Name" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "Defined" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Opened" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope)) :+: C1 ('MetaCons "Applied" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope))))

class IsNoName a where Source #

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

Minimal complete definition

Nothing

Methods

isNoName :: a -> Bool Source #

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

Instances

Instances details
IsNoName ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

isNoName :: ModuleName -> 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 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 RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

isNoName :: RawTopLevelModuleName -> 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, …