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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Internal.Names

Description

Extract all names from things.

Documentation

class NamesIn a where #

Minimal complete definition

namesIn

Methods

namesIn :: a -> Set QName #

Instances

NamesIn AmbiguousQName # 
NamesIn QName # 

Methods

namesIn :: QName -> Set QName #

NamesIn Literal # 

Methods

namesIn :: Literal -> Set QName #

NamesIn Clause # 

Methods

namesIn :: Clause -> Set QName #

NamesIn LevelAtom # 

Methods

namesIn :: LevelAtom -> Set QName #

NamesIn PlusLevel # 

Methods

namesIn :: PlusLevel -> Set QName #

NamesIn Level # 

Methods

namesIn :: Level -> Set QName #

NamesIn Sort # 

Methods

namesIn :: Sort -> Set QName #

NamesIn Term # 

Methods

namesIn :: Term -> Set QName #

NamesIn ConHead # 

Methods

namesIn :: ConHead -> Set QName #

NamesIn CompiledClauses # 
NamesIn Defn # 

Methods

namesIn :: Defn -> Set QName #

NamesIn Definition # 
NamesIn DisplayTerm # 
NamesIn DisplayForm # 
NamesIn PSyn # 

Methods

namesIn :: PSyn -> Set QName #

NamesIn a => NamesIn [a] # 

Methods

namesIn :: [a] -> Set QName #

NamesIn a => NamesIn (Maybe a) # 

Methods

namesIn :: Maybe a -> Set QName #

NamesIn a => NamesIn (Dom a) # 

Methods

namesIn :: Dom a -> Set QName #

NamesIn a => NamesIn (Arg a) # 

Methods

namesIn :: Arg a -> Set QName #

NamesIn a => NamesIn (FieldAssignment' a) # 
NamesIn (Pattern' a) # 

Methods

namesIn :: Pattern' a -> Set QName #

NamesIn a => NamesIn (Tele a) # 

Methods

namesIn :: Tele a -> Set QName #

NamesIn a => NamesIn (Type' a) # 

Methods

namesIn :: Type' a -> Set QName #

NamesIn a => NamesIn (Abs a) # 

Methods

namesIn :: Abs a -> Set QName #

NamesIn a => NamesIn (Elim' a) # 

Methods

namesIn :: Elim' a -> Set QName #

NamesIn (Pattern' a) # 

Methods

namesIn :: Pattern' a -> Set QName #

NamesIn a => NamesIn (Case a) # 

Methods

namesIn :: Case a -> Set QName #

NamesIn a => NamesIn (WithArity a) # 

Methods

namesIn :: WithArity a -> Set QName #

NamesIn a => NamesIn (Local a) # 

Methods

namesIn :: Local a -> Set QName #

NamesIn a => NamesIn (Open a) # 

Methods

namesIn :: Open a -> Set QName #

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

Methods

namesIn :: (a, b) -> Set QName #

NamesIn a => NamesIn (Named n a) # 

Methods

namesIn :: Named n a -> Set QName #

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

Methods

namesIn :: (a, b, c) -> Set QName #

newtype PSyn #

Constructors

PSyn PatternSynDefn 

Instances

NamesIn PSyn # 

Methods

namesIn :: PSyn -> Set QName #