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

Safe HaskellNone
LanguageHaskell98

Agda.Syntax.Internal.Names

Description

Extract all names from things.

Documentation

class NamesIn a where Source #

Minimal complete definition

namesIn

Methods

namesIn :: a -> Set QName Source #

Instances

NamesIn AmbiguousQName Source # 
NamesIn QName Source # 

Methods

namesIn :: QName -> Set QName Source #

NamesIn Literal Source # 
NamesIn Clause Source # 
NamesIn LevelAtom Source # 
NamesIn PlusLevel Source # 
NamesIn Level Source # 

Methods

namesIn :: Level -> Set QName Source #

NamesIn Sort Source # 

Methods

namesIn :: Sort -> Set QName Source #

NamesIn Term Source # 

Methods

namesIn :: Term -> Set QName Source #

NamesIn ConHead Source # 
NamesIn CompiledClauses Source # 
NamesIn Defn Source # 

Methods

namesIn :: Defn -> Set QName Source #

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

Methods

namesIn :: PSyn -> Set QName Source #

NamesIn a => NamesIn [a] Source # 

Methods

namesIn :: [a] -> Set QName Source #

NamesIn a => NamesIn (Maybe a) Source # 

Methods

namesIn :: Maybe a -> Set QName Source #

NamesIn a => NamesIn (Dom a) Source # 

Methods

namesIn :: Dom a -> Set QName Source #

NamesIn a => NamesIn (Arg a) Source # 

Methods

namesIn :: Arg a -> Set QName Source #

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

Methods

namesIn :: Pattern' a -> Set QName Source #

NamesIn (Pattern' a) Source # 

Methods

namesIn :: Pattern' a -> Set QName Source #

NamesIn a => NamesIn (ClauseBodyF a) Source # 
NamesIn a => NamesIn (Tele a) Source # 

Methods

namesIn :: Tele a -> Set QName Source #

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

Methods

namesIn :: Type' a -> Set QName Source #

NamesIn a => NamesIn (Abs a) Source # 

Methods

namesIn :: Abs a -> Set QName Source #

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

Methods

namesIn :: Elim' a -> Set QName Source #

NamesIn a => NamesIn (Case a) Source # 

Methods

namesIn :: Case a -> Set QName Source #

NamesIn a => NamesIn (WithArity a) Source # 
NamesIn a => NamesIn (Open a) Source # 

Methods

namesIn :: Open a -> Set QName Source #

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

Methods

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

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

Methods

namesIn :: Named n a -> Set QName Source #

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

Methods

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

newtype PSyn Source #

Constructors

PSyn PatternSynDefn 

Instances