Agda-2.5.2: A dependently typed functional programming language and proof assistant
Agda.Syntax.Internal.Names
Description
Extract all names from things.
class NamesIn a where Source #
Minimal complete definition
namesIn
Methods
namesIn :: a -> Set QName Source #
Instances
namesIn :: AmbiguousQName -> Set QName Source #
namesIn :: QName -> Set QName Source #
namesIn :: Literal -> Set QName Source #
namesIn :: Clause -> Set QName Source #
namesIn :: LevelAtom -> Set QName Source #
namesIn :: PlusLevel -> Set QName Source #
namesIn :: Level -> Set QName Source #
namesIn :: Sort -> Set QName Source #
namesIn :: Term -> Set QName Source #
namesIn :: ConHead -> Set QName Source #
namesIn :: CompiledClauses -> Set QName Source #
namesIn :: Defn -> Set QName Source #
namesIn :: Definition -> Set QName Source #
namesIn :: DisplayTerm -> Set QName Source #
namesIn :: DisplayForm -> Set QName Source #
namesIn :: PSyn -> Set QName Source #
namesIn :: [a] -> Set QName Source #
namesIn :: Maybe a -> Set QName Source #
namesIn :: Dom a -> Set QName Source #
namesIn :: Arg a -> Set QName Source #
namesIn :: FieldAssignment' a -> Set QName Source #
namesIn :: Pattern' a -> Set QName Source #
namesIn :: Tele a -> Set QName Source #
namesIn :: Type' a -> Set QName Source #
namesIn :: Abs a -> Set QName Source #
namesIn :: Elim' a -> Set QName Source #
namesIn :: Case a -> Set QName Source #
namesIn :: WithArity a -> Set QName Source #
namesIn :: Local a -> Set QName Source #
namesIn :: Open a -> Set QName Source #
namesIn :: (a, b) -> Set QName Source #
namesIn :: Named n a -> Set QName Source #
namesIn :: (a, b, c) -> Set QName Source #
namesInFoldable :: (Foldable f, NamesIn a) => f a -> Set QName Source #
newtype PSyn Source #
Constructors