Agda.Syntax.Internal.Names

Extract all names from things.

Documentation

namesIn :: (NamesIn a, Collection QName m) => a -> m

class NamesIn a where

Minimal complete definition

Nothing

Methods

namesIn' :: Monoid m => (QName -> m) -> a -> m

default namesIn' :: (Monoid m, Foldable f, NamesIn b, f b ~ a) => (QName -> m) -> a -> m

Instances

NamesIn AmbiguousQName

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> AmbiguousQName -> m

NamesIn QName

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn Literal

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Literal -> m

NamesIn Clause

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Clause -> m

NamesIn PlusLevel

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> PlusLevel -> m

NamesIn Level

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Level -> m

NamesIn Sort

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Sort -> m

NamesIn Term

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Term -> m

NamesIn ConHead

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> ConHead -> m

NamesIn CompiledClauses

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> CompiledClauses -> m

NamesIn Defn

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Defn -> m

NamesIn CompKit

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> CompKit -> m

NamesIn Definition

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Definition -> m

NamesIn DisplayTerm

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> DisplayTerm -> m

NamesIn DisplayForm

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> DisplayForm -> m

NamesIn PSyn

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> PSyn -> m

NamesIn a => NamesIn [a]

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> [a] -> m

NamesIn a => NamesIn (Maybe a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Maybe a -> m

NamesIn a => NamesIn (NonEmpty a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> NonEmpty a -> m

NamesIn a => NamesIn (Set a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Set a -> m

NamesIn a => NamesIn (Arg a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Arg a -> m

NamesIn a => NamesIn (FieldAssignment' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> FieldAssignment' a -> m

NamesIn a => NamesIn (Elim' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Elim' a -> m

NamesIn (Pattern' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Pattern' a -> m

NamesIn a => NamesIn (Tele a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Tele a -> m

NamesIn a => NamesIn (Type' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Type' a -> m

NamesIn a => NamesIn (Abs a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Abs a -> m

NamesIn a => NamesIn (Dom a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Dom a -> m

NamesIn a => NamesIn (Case a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Case a -> m

NamesIn a => NamesIn (WithArity a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> WithArity a -> m

NamesIn (Pattern' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Pattern' a -> m

NamesIn a => NamesIn (Open a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Open a -> m

(NamesIn a, NamesIn b) => NamesIn (a, b)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> (a, b) -> m

NamesIn a => NamesIn (Map k a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Map k a -> m

NamesIn a => NamesIn (Named n a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Named n a -> m

(NamesIn a, NamesIn b, NamesIn c) => NamesIn (a, b, c)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> (a, b, c) -> m

(NamesIn a, NamesIn b, NamesIn c, NamesIn d) => NamesIn (a, b, c, d)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> (a, b, c, d) -> m

newtype PSyn

Constructors

PSyn PatternSynDefn

Instances

NamesIn PSyn

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> PSyn -> m