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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Internal.Names

Description

Extract all names from things.

# Documentation

class NamesIn a where Source #

Minimal complete definition

Nothing

Methods

namesIn :: a -> Set QName Source #

namesIn :: (Foldable f, NamesIn b, f b ~ a) => a -> Set QName Source #

Instances

NamesIn AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: AmbiguousQName -> Set QName Source #
NamesIn QName Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: QName -> Set QName Source #
NamesIn Literal Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Literal -> Set QName Source #
NamesIn Clause Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Clause -> Set QName Source #
NamesIn LevelAtom Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: LevelAtom -> Set QName Source #
NamesIn PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: PlusLevel -> Set QName Source #
NamesIn Level Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Level -> Set QName Source #
NamesIn Sort Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Sort -> Set QName Source #
NamesIn Term Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Term -> Set QName Source #
NamesIn ConHead Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: ConHead -> Set QName Source #
NamesIn CompiledClauses Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: CompiledClauses -> Set QName Source #
NamesIn Defn Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Defn -> Set QName Source #
NamesIn CompKit Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: CompKit -> Set QName Source #
NamesIn Definition Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Definition -> Set QName Source #
NamesIn DisplayTerm Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: DisplayTerm -> Set QName Source #
NamesIn DisplayForm Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: DisplayForm -> Set QName Source #
NamesIn PSyn Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: PSyn -> Set QName Source #
NamesIn a => NamesIn [a] Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: [a] -> Set QName Source #
NamesIn a => NamesIn (Maybe a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Maybe a -> Set QName Source #
NamesIn a => NamesIn (NonemptyList a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: NonemptyList a -> Set QName Source #
NamesIn a => NamesIn (Dom a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Dom a -> Set QName Source #
NamesIn a => NamesIn (Arg a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Arg a -> Set QName Source #
NamesIn a => NamesIn (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: FieldAssignment' a -> Set QName Source #
NamesIn (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Pattern' a -> Set QName Source #
NamesIn a => NamesIn (Tele a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Tele a -> Set QName Source #
NamesIn a => NamesIn (Type' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Type' a -> Set QName Source #
NamesIn a => NamesIn (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Abs a -> Set QName Source #
NamesIn a => NamesIn (Elim' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Elim' a -> Set QName Source #
NamesIn a => NamesIn (Case a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Case a -> Set QName Source #
NamesIn a => NamesIn (WithArity a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: WithArity a -> Set QName Source #
NamesIn (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Pattern' a -> Set QName Source #
NamesIn a => NamesIn (Open a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Open a -> Set QName Source #
(NamesIn a, NamesIn b) => NamesIn (a, b) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: (a, b) -> Set QName Source #
NamesIn a => NamesIn (Named n a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Named n a -> Set QName Source #
(NamesIn a, NamesIn b, NamesIn c) => NamesIn (a, b, c) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: (a, b, c) -> Set QName Source #

newtype PSyn Source #

Constructors

PSyn PatternSynDefn |

Instances

NamesIn PSyn Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: PSyn -> Set QName Source #