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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Concrete.Name

Contents

Description

Names in the concrete syntax are just strings (or lists of strings for qualified names).

Synopsis

Documentation

data Name Source #

A name is a non-empty list of alternating Ids and Holes. A normal name is represented by a singleton list, and operators are represented by a list with Holes where the arguments should go. For instance: [Hole,Id "+",Hole] is infix addition.

Equality and ordering on Names are defined to ignore range so same names in different locations are equal.

Constructors

Name

A (mixfix) identifier.

NoName

_.

Fields

Instances
Eq Name Source #

Define equality on Name to ignore range so same names in different locations are equal.

Is there a reason not to do this? -Jeff

No. But there are tons of reasons to do it. For instance, when using names as keys in maps you really don't want to have to get the range right to be able to do a lookup. -Ulf

Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

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

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

Data Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

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

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

toConstr :: Name -> Constr

dataTypeOf :: Name -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.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 # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

NFData Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

rnf :: Name -> ()

NFData AsName

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: AsName -> ()

Pretty Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: Name -> Doc Source #

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

prettyList :: [Name] -> Doc Source #

KillRange Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

KillRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

SetRange Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

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

HasRange Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: Name -> Range Source #

HasRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

Underscore Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

IsNoName Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Name -> Bool Source #

LensInScope Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

NumHoles Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: Name -> Int Source #

ExprLike Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> Name -> Name Source #

traverseExpr :: Monad m => (Expr -> m Expr) -> Name -> m Name Source #

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

SubstExpr Name Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

EmbPrj Name Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32 Source #

icod_ :: Name -> S Int32 Source #

value :: Int32 -> R Name Source #

PrettyTCM Name Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Name -> TCM Doc Source #

ToConcrete Name Name Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Pretty (ThingWithFixity Name) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ToAbstract (NewName Name) Name Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

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

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

isOpenMixfix :: Name -> Bool Source #

An open mixfix identifier is either prefix, infix, or suffix. That is to say: at least one of its extremities is a Hole

data NamePart Source #

Mixfix identifiers are composed of words and holes, e.g. _+_ or if_then_else_ or [_/_].

Constructors

Hole

_ part.

Id RawName

Identifier part.

Instances
Eq NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

(==) :: NamePart -> NamePart -> Bool

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

Data NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NamePart -> c NamePart

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

toConstr :: NamePart -> Constr

dataTypeOf :: NamePart -> DataType

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

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

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

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

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

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

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

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

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

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

Ord NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

compare :: NamePart -> NamePart -> Ordering

(<) :: NamePart -> NamePart -> Bool

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

(>) :: NamePart -> NamePart -> Bool

(>=) :: NamePart -> NamePart -> Bool

max :: NamePart -> NamePart -> NamePart

min :: NamePart -> NamePart -> NamePart

Show NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

showsPrec :: Int -> NamePart -> ShowS

show :: NamePart -> String

showList :: [NamePart] -> ShowS

Generic NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Associated Types

type Rep NamePart :: Type -> Type

Methods

from :: NamePart -> Rep NamePart x

to :: Rep NamePart x -> NamePart

NFData NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

rnf :: NamePart -> ()

Pretty NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

EmbPrj NamePart Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NamePart -> S Int32 Source #

icod_ :: NamePart -> S Int32 Source #

value :: Int32 -> R NamePart Source #

NumHoles [NamePart] Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: [NamePart] -> Int Source #

type Rep NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

type Rep NamePart = D1 (MetaData "NamePart" "Agda.Syntax.Concrete.Name" "Agda-2.6.0.1-B0t7sLPZhcP4jvj0wGvNPO" False) (C1 (MetaCons "Hole" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Id" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 RawName)))

data QName Source #

QName is a list of namespaces and the name of the constant. For the moment assumes namespaces are just Names and not explicitly applied modules. Also assumes namespaces are generative by just using derived equality. We will have to define an equality instance to non-generative namespaces (as well as having some sort of lookup table for namespace names).

Constructors

Qual Name QName

A.rest.

QName Name

x.

Instances
Eq QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

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

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

Data QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

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

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

toConstr :: QName -> Constr

dataTypeOf :: QName -> DataType

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

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

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

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

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

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

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

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

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

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

Ord QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.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.Concrete.Name

Methods

showsPrec :: Int -> QName -> ShowS

show :: QName -> String

showList :: [QName] -> ShowS

NFData QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

rnf :: QName -> ()

Pretty QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

KillRange QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

SetRange QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

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

HasRange QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: QName -> Range Source #

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

LensInScope QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

NumHoles QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: QName -> Int Source #

ExprLike QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

EmbPrj QName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QName -> S Int32 Source #

icod_ :: QName -> S Int32 Source #

value :: Int32 -> R QName Source #

PrettyTCM QName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: QName -> TCM Doc Source #

ToConcrete ModuleName QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete QName QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete ResolvedName QName Source #

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete AbstractName QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

data TopLevelModuleName Source #

Top-level module names. Used in connection with the file system.

Invariant: The list must not be empty.

Constructors

TopLevelModuleName 

Fields

Instances
Eq TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Data TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TopLevelModuleName -> c TopLevelModuleName

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

toConstr :: TopLevelModuleName -> Constr

dataTypeOf :: TopLevelModuleName -> DataType

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

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

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

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

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

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

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

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

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

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

Ord TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Show TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

showsPrec :: Int -> TopLevelModuleName -> ShowS

show :: TopLevelModuleName -> String

showList :: [TopLevelModuleName] -> ShowS

Pretty TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Sized TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

size :: TopLevelModuleName -> Int Source #

KillRange TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

SetRange TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

HasRange TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

EmbPrj TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Operations on Name and NamePart

stringNameParts :: String -> [NamePart] Source #

Parse a string to parts of a concrete name.

Note: stringNameParts "_" == [Id "_"] == nameParts NoName{}

class NumHoles a where Source #

Number of holes in a Name (i.e., arity of a mixfix-operator).

Methods

numHoles :: a -> Int Source #

Instances
NumHoles QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: QName -> Int Source #

NumHoles Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

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

NumHoles QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: QName -> Int Source #

NumHoles Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: Name -> Int Source #

NumHoles [NamePart] Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: [NamePart] -> Int Source #

isOperator :: Name -> Bool Source #

Is the name an operator?

isHole :: NamePart -> Bool Source #

isPrefix :: Name -> Bool Source #

isPostfix :: Name -> Bool Source #

isInfix :: Name -> Bool Source #

isNonfix :: Name -> Bool Source #

Keeping track of which names are (not) in scope

data NameInScope Source #

Constructors

InScope 
NotInScope 
Instances
Eq NameInScope Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

(==) :: NameInScope -> NameInScope -> Bool

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

Data NameInScope Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameInScope -> c NameInScope

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

toConstr :: NameInScope -> Constr

dataTypeOf :: NameInScope -> DataType

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

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

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

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

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

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

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

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

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

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

Show NameInScope Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

showsPrec :: Int -> NameInScope -> ShowS

show :: NameInScope -> String

showList :: [NameInScope] -> ShowS

NFData NameInScope Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

rnf :: NameInScope -> ()

LensInScope NameInScope Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

EmbPrj NameInScope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NameInScope -> S Int32 Source #

icod_ :: NameInScope -> S Int32 Source #

value :: Int32 -> R NameInScope Source #

class LensInScope a where Source #

Minimal complete definition

lensInScope

Instances
LensInScope NameInScope Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

LensInScope QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

LensInScope Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

LensInScope QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

LensInScope Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Generating fresh names

nextStr :: String -> String Source #

nextName :: Name -> Name Source #

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

firstNonTakenName :: (Name -> Bool) -> Name -> Name Source #

Get the first version of the concrete name that does not satisfy the given predicate.

nameRoot :: Name -> RawName Source #

Get a raw version of the name with all suffixes removed. For instance, nameRoot "x₁₂₃" = "x". The name must not be a NoName.

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

Operations on qualified names

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

qualify A.B x == A.B.x

unqualify :: QName -> Name Source #

unqualify A.B.x == x

The range is preserved.

qnameParts :: QName -> [Name] Source #

qnameParts A.B.x = [A, B, x]

isQualified :: QName -> Bool Source #

Is the name qualified?

Operations on TopLevelModuleName

toTopLevelModuleName :: QName -> TopLevelModuleName Source #

Turns a qualified name into a TopLevelModuleName. The qualified name is assumed to represent a top-level module name.

moduleNameToFileName :: TopLevelModuleName -> String -> FilePath Source #

Turns a top-level module name into a file name with the given suffix.

projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath Source #

Finds the current project's "root" directory, given a project file and the corresponding top-level module name.

Example: If the module "A.B.C" is located in the file "fooABC.agda", then the root is "foo".

Precondition: The module name must be well-formed.

No name stuff

class IsNoName a where Source #

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

Methods

isNoName :: a -> Bool Source #

Instances
IsNoName String Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: String -> Bool Source #

IsNoName ByteString Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: ByteString -> Bool Source #

IsNoName QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: QName -> Bool Source #

IsNoName Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Name -> Bool Source #

IsNoName Name Source #

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

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

isNoName :: Name -> Bool Source #

Showing names

Printing names

Range instances

NFData instances