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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Concrete.Name

Contents

- Constructing simple `Name`s.
- Operations on `Name` and `NamePart`
- Keeping track of which names are (not) in scope
- Generating fresh names
- Operations on qualified names
- No name stuff
- Showing names
- Printing names
- Range instances
- NFData instances

Description

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

Synopsis

- data Name
  - = Name {
    - nameRange :: Range
    - nameInScope :: NameInScope
    - nameNameParts :: NameParts
    }
  - | NoName {
    - nameRange :: Range
    - nameId :: NameId
    }
- type NameParts = List1 NamePart
- isOpenMixfix :: Name -> Bool
- data NamePart
  - = Hole
  - | Id RawName
- data QName
  - = Qual Name QName
  - | QName Name
- simpleName :: RawName -> Name
- simpleBinaryOperator :: RawName -> Name
- simpleHole :: Name
- lensNameParts :: Lens' Name NameParts
- nameToRawName :: Name -> RawName
- nameParts :: Name -> NameParts
- nameStringParts :: Name -> [RawName]
- stringNameParts :: String -> NameParts
- class NumHoles a where
  - numHoles :: a -> Int
- isOperator :: Name -> Bool
- isHole :: NamePart -> Bool
- isPrefix :: Name -> Bool
- isPostfix :: Name -> Bool
- isInfix :: Name -> Bool
- isNonfix :: Name -> Bool
- data NameInScope
  - = InScope
  - | NotInScope
- class LensInScope a where
  - lensInScope :: Lens' a NameInScope
  - isInScope :: a -> NameInScope
  - mapInScope :: (NameInScope -> NameInScope) -> a -> a
  - setInScope :: a -> a
  - setNotInScope :: a -> a
- data FreshNameMode
  - = UnicodeSubscript
  - | AsciiCounter
- nextRawName :: FreshNameMode -> RawName -> RawName
- nextName :: FreshNameMode -> Name -> Name
- lastIdPart :: Lens' NameParts RawName
- firstNonTakenName :: FreshNameMode -> (Name -> Bool) -> Name -> Name
- nameSuffix :: Lens' Name (Maybe Suffix)
- nameSuffixView :: Name -> (Maybe Suffix, Name)
- setNameSuffix :: Maybe Suffix -> Name -> Name
- nameRoot :: Name -> RawName
- sameRoot :: Name -> Name -> Bool
- lensQNameName :: Lens' QName Name
- qualify :: QName -> Name -> QName
- unqualify :: QName -> Name
- qnameParts :: QName -> List1 Name
- isQualified :: QName -> Bool
- isUnqualified :: QName -> Maybe Name
- noName_ :: Name
- noName :: Range -> Name
- class IsNoName a where
  - isNoName :: a -> Bool

# Documentation

data Name Source #

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

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

Constructors

Name | A (mixfix) identifier.

Fields

- nameRange :: Range
- nameInScope :: NameInScope
- nameNameParts :: NameParts

NoName | `_`.

Fields

- nameRange :: Range
- nameId :: NameId

#### Instances

Instances details

SubstExpr Name Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Name -> Name Source #
Underscore Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods underscore :: Name Source # isUnderscore :: Name -> Bool Source #
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 #
ExprLike Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Name -> Name Source # foldExpr :: Monoid m => (Expr -> m) -> Name -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Name -> m Name Source #
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 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.Concrete.Name Methods numHoles :: Name -> Int Source #
HasRange AsName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: AsName -> Range Source #
HasRange Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods getRange :: Name -> Range Source #
KillRange AsName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT AsName Source #
KillRange Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods killRange :: KillRangeT Name Source #
SetRange Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods setRange :: Range -> Name -> Name Source #
ToAbstract HoleContent Source # | Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon HoleContent = HoleContent

Methods

toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent) Source #

ToAbstract RewriteEqn Source # |

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RewriteEqn |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon RewriteEqn = RewriteEqn' () BindName Pattern Expr

Methods

toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn) Source #

PrettyTCM ImportedName Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ImportedName -> m Doc Source #
PrettyTCM Name Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Name -> m Doc 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 #
NFData AsName Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: AsName -> () Source #
NFData Name Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete.Name Methods rnf :: Name -> () Source #
Show Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods showsPrec :: Int -> Name -> ShowS Source # show :: Name -> String Source # showList :: [Name] -> ShowS Source #
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 Source # (/=) :: Name -> Name -> Bool Source #
Ord Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods compare :: Name -> Name -> Ordering Source # (<) :: Name -> Name -> Bool Source # (<=) :: Name -> Name -> Bool Source # (>) :: Name -> Name -> Bool Source # (>=) :: Name -> Name -> Bool Source # max :: Name -> Name -> Name Source # min :: Name -> Name -> Name Source #
Pretty (ThingWithFixity Name) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ThingWithFixity Name -> Doc Source # prettyPrec :: Int -> ThingWithFixity Name -> Doc Source # prettyList :: [ThingWithFixity Name] -> Doc Source #
type AbsOfCon HoleContent Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon HoleContent = HoleContent
type AbsOfCon RewriteEqn Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon RewriteEqn = RewriteEqn' () BindName Pattern Expr

type NameParts = List1 NamePart 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

Instances details

Pretty NamePart Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods pretty :: NamePart -> Doc Source # prettyPrec :: Int -> NamePart -> Doc Source # prettyList :: [NamePart] -> Doc Source #
NumHoles NameParts Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods numHoles :: NameParts -> Int Source #
EmbPrj NamePart Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NamePart -> S Word32 Source # icod_ :: NamePart -> S Word32 Source # value :: Word32 -> R NamePart Source #
NFData NamePart Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods rnf :: NamePart -> () Source #
Generic NamePart Source # |

Instance details

Defined in Agda.Syntax.Concrete.Name

Associated Types

type Rep NamePart |
Instance details Defined in Agda.Syntax.Concrete.Name type Rep NamePart = D1 ('MetaData "NamePart" "Agda.Syntax.Concrete.Name" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Hole" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Id" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RawName)))

Methods

from :: NamePart -> Rep NamePart x Source #

to :: Rep NamePart x -> NamePart Source #

Show NamePart Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods showsPrec :: Int -> NamePart -> ShowS Source # show :: NamePart -> String Source # showList :: [NamePart] -> ShowS Source #
Eq NamePart Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods (==) :: NamePart -> NamePart -> Bool Source # (/=) :: NamePart -> NamePart -> Bool Source #
Ord NamePart Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods compare :: NamePart -> NamePart -> Ordering Source # (<) :: NamePart -> NamePart -> Bool Source # (<=) :: NamePart -> NamePart -> Bool Source # (>) :: NamePart -> NamePart -> Bool Source # (>=) :: NamePart -> NamePart -> Bool Source # max :: NamePart -> NamePart -> NamePart Source # min :: NamePart -> NamePart -> NamePart 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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 `Name`s 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

Instances details

Underscore QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods underscore :: QName Source # isUnderscore :: QName -> Bool Source #
Pretty QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods pretty :: QName -> Doc Source # prettyPrec :: Int -> QName -> Doc Source # prettyList :: [QName] -> Doc Source #
ExprLike QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> QName -> QName Source # foldExpr :: Monoid m => (Expr -> m) -> QName -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> QName -> m QName Source #
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 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.Concrete.Name Methods numHoles :: QName -> Int Source #
HasRange QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods getRange :: QName -> Range Source #
KillRange QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods killRange :: KillRangeT QName Source #
SetRange QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods setRange :: Range -> QName -> QName Source #
PrettyTCM QName Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => QName -> m Doc 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 #
NFData QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods rnf :: QName -> () Source #
Show QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods showsPrec :: Int -> QName -> ShowS Source # show :: QName -> String Source # showList :: [QName] -> ShowS Source #
Eq QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods (==) :: QName -> QName -> Bool Source # (/=) :: QName -> QName -> Bool Source #
Ord QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods compare :: QName -> QName -> Ordering Source # (<) :: QName -> QName -> Bool Source # (<=) :: QName -> QName -> Bool Source # (>) :: QName -> QName -> Bool Source # (>=) :: QName -> QName -> Bool Source # max :: QName -> QName -> QName Source # min :: QName -> QName -> QName Source #

# Constructing simple `Name`s.

simpleName :: RawName -> Name Source #

Create an ordinary `InScope` name.

simpleBinaryOperator :: RawName -> Name Source #

Create a binary operator name in scope.

simpleHole :: Name Source #

Create an ordinary `InScope` name containing a single `Hole`.

# Operations on `Name` and `NamePart`

lensNameParts :: Lens' Name NameParts Source #

Don't use on 'NoName{}'.

nameToRawName :: Name -> RawName Source #

nameParts :: Name -> NameParts Source #

nameStringParts :: Name -> [RawName] Source #

stringNameParts :: String -> NameParts 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

Instances details

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 Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods numHoles :: Name -> 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.Concrete.Name Methods numHoles :: Name -> Int Source #
NumHoles NameParts Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods numHoles :: NameParts -> Int Source #
NumHoles QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods numHoles :: QName -> Int Source #

isOperator :: Name -> Bool Source #

Is the name an operator? Needs at least 2 `NamePart`s.

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

Instances details

EncodeTCM NameInScope Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: NameInScope -> TCM Value Source #
LensInScope NameInScope Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods lensInScope :: Lens' NameInScope NameInScope Source # isInScope :: NameInScope -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> NameInScope -> NameInScope Source # setInScope :: NameInScope -> NameInScope Source # setNotInScope :: NameInScope -> NameInScope Source #
EmbPrj NameInScope Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NameInScope -> S Word32 Source # icod_ :: NameInScope -> S Word32 Source # value :: Word32 -> R NameInScope Source #
ToJSON NameInScope Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: NameInScope -> Value Source # toEncoding :: NameInScope -> Encoding Source # toJSONList :: [NameInScope] -> Value Source # toEncodingList :: [NameInScope] -> Encoding Source # omitField :: NameInScope -> Bool Source #
NFData NameInScope Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods rnf :: NameInScope -> () Source #
Show NameInScope Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods showsPrec :: Int -> NameInScope -> ShowS Source # show :: NameInScope -> String Source # showList :: [NameInScope] -> ShowS Source #
Eq NameInScope Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods (==) :: NameInScope -> NameInScope -> Bool Source # (/=) :: NameInScope -> NameInScope -> Bool Source #

class LensInScope a where Source #

Minimal complete definition

lensInScope

Methods

lensInScope :: Lens' a NameInScope Source #

isInScope :: a -> NameInScope Source #

mapInScope :: (NameInScope -> NameInScope) -> a -> a Source #

setInScope :: a -> a Source #

setNotInScope :: a -> a Source #

#### Instances

Instances details

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 #
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 #
LensInScope Name Source # |
Instance details Defined in Agda.Syntax.Concrete.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 #
LensInScope NameInScope Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods lensInScope :: Lens' NameInScope NameInScope Source # isInScope :: NameInScope -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> NameInScope -> NameInScope Source # setInScope :: NameInScope -> NameInScope Source # setNotInScope :: NameInScope -> NameInScope Source #
LensInScope QName Source # |
Instance details Defined in Agda.Syntax.Concrete.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 #

# Generating fresh names

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

nextRawName :: FreshNameMode -> RawName -> RawName 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`.

lastIdPart :: Lens' NameParts RawName Source #

Zoom on the last non-hole in a name.

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

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

nameSuffix :: Lens' Name (Maybe Suffix) Source #

Lens for accessing and modifying the suffix of a name. The suffix of a `NoName` is always `Nothing`, and should not be changed.

nameSuffixView :: Name -> (Maybe Suffix, Name) Source #

Split a name into a base name plus a suffix.

setNameSuffix :: Maybe Suffix -> Name -> Name Source #

Replaces the suffix of a name. Unless the suffix is `Nothing`, the name should not be `NoName`.

nameRoot :: Name -> RawName Source #

Get a raw version of the name with all suffixes removed. For instance, `nameRoot "x₁₂₃" = "x"`.

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

# Operations on qualified names

lensQNameName :: Lens' QName Name Source #

Lens for the unqualified part of a QName

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

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

isQualified :: QName -> Bool Source #

Is the name (un)qualified?

isUnqualified :: QName -> Maybe Name Source #

# No name stuff

noName_ :: Name Source #

    noName_ = noName noRange

noName :: Range -> Name Source #

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 #

# Showing names

# Printing names

# Range instances

# NFData instances