Agda.Syntax.Internal.Names

Extract all names and meta-variables from things.

Documentation

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

Some or all of the QNames that can be found in the given thing.

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

Some or all of the QNames that can be found in the given thing.

metasIn :: (NamesIn a, Collection MetaId m) => a -> m

Some or all of the meta-variables that can be found in the given thing.

metasIn' :: (NamesIn a, Monoid m) => (MetaId -> m) -> a -> m

Some or all of the meta-variables that can be found in the given thing.

namesAndMetasIn :: (NamesIn a, Collection QName m1, Collection MetaId m2) => a -> (m1, m2)

Some or all of the names and meta-variables that can be found in the given thing.

class NamesIn a where

Minimal complete definition

Nothing

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> a -> m

Some or all of the names and meta-variables that can be found in the given thing.

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

Instances

NamesIn AmbiguousQName

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> AmbiguousQName -> m

NamesIn QName

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> QName -> m

NamesIn MetaId

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> MetaId -> m

NamesIn Clause

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Clause -> m

NamesIn ConHead

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> ConHead -> m

NamesIn Level

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Level -> m

NamesIn PlusLevel

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> PlusLevel -> m

NamesIn Sort

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Sort -> m

NamesIn Term

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Term -> m

NamesIn PSyn

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> PSyn -> m

NamesIn Literal

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Literal -> m

NamesIn CaseInfo

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CaseInfo -> m

NamesIn CaseType

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CaseType -> m

NamesIn Compiled

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Compiled -> m

NamesIn TAlt

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> TAlt -> m

NamesIn TTerm

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> TTerm -> m

NamesIn CompiledClauses

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CompiledClauses -> m

NamesIn CompKit

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CompKit -> m

NamesIn Definition

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Definition -> m

NamesIn Defn

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Defn -> m

NamesIn DisplayForm

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> DisplayForm -> m

NamesIn DisplayTerm

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> DisplayTerm -> m

NamesIn ExtLamInfo

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> ExtLamInfo -> m

NamesIn NLPSort

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> NLPSort -> m

NamesIn NLPType

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> NLPType -> m

NamesIn NLPat

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> NLPat -> m

NamesIn PrimFun

Note that the primFunImplementation is skipped.

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> PrimFun -> m

NamesIn RewriteRule

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> RewriteRule -> m

NamesIn Section

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Section -> m

NamesIn System

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> System -> m

NamesIn Bool

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Bool -> m

NamesIn (Pattern' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Pattern' a -> m

NamesIn a => NamesIn (Arg a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Arg a -> m

NamesIn a => NamesIn (FieldAssignment' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> FieldAssignment' a -> m

NamesIn a => NamesIn (Abs a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Abs a -> m

NamesIn (Pattern' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Pattern' a -> m

NamesIn a => NamesIn (Substitution' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Substitution' a -> m

NamesIn a => NamesIn (Tele a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Tele a -> m

NamesIn a => NamesIn (Type' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Type' a -> m

NamesIn a => NamesIn (Elim' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Elim' a -> m

NamesIn a => NamesIn (Case a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Case a -> m

NamesIn a => NamesIn (WithArity a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> WithArity a -> m

NamesIn a => NamesIn (Builtin a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Builtin a -> m

NamesIn a => NamesIn (FunctionInverse' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> FunctionInverse' a -> m

NamesIn a => NamesIn (Open a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Open a -> m

NamesIn a => NamesIn (List1 a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> List1 a -> m

NamesIn a => NamesIn (Set a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Set a -> m

NamesIn a => NamesIn (Maybe a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Maybe a -> m

NamesIn a => NamesIn (Maybe a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Maybe a -> m

NamesIn a => NamesIn [a]

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> [a] -> m

NamesIn a => NamesIn (Named n a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Named n a -> m

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

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Dom' a b -> m

NamesIn a => NamesIn (Map k a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Map k a -> m

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

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> HashMap a b -> m

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

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> (a, b) -> m

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

Defined in Agda.Syntax.Internal.Names

Methods

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

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> (a, b, c, d) -> m

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

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> (a, b, c, d, e) -> m

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

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> (a, b, c, d, e, f) -> m

newtype PSyn

Constructors

PSyn PatternSynDefn

Instances

NamesIn PSyn

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> PSyn -> m