Agda-2.6.2.1.20220327: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Internal.Names

Description

Extract all names from things.

Documentation

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

class NamesIn a where Source #

Minimal complete definition

Nothing

Methods

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

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

Instances

Instances details
NamesIn AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn QName Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn Clause Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn Level Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn Sort Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn Term Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn PSyn Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn Literal Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn CompiledClauses Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn CompKit Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn Definition Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn Defn Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn DisplayForm Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn DisplayTerm Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn (Abs a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn (Dom a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn (Tele a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn (Type' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn (Elim' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn (Case a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn (WithArity a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn (Open a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn (Set a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn (NonEmpty a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn [a] Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn (Named n a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn a => NamesIn (Map k a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

(NamesIn a, NamesIn b) => NamesIn (a, b) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

(NamesIn a, NamesIn b, NamesIn c) => NamesIn (a, b, c) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

(NamesIn a, NamesIn b, NamesIn c, NamesIn d) => NamesIn (a, b, c, d) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

newtype PSyn Source #

Constructors

PSyn PatternSynDefn 

Instances

Instances details
NamesIn PSyn Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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