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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Internal.Names

Description

Extract all names and meta-variables from things.

Synopsis

- namesIn :: (NamesIn a, Collection QName m) => a -> m
- namesIn' :: (NamesIn a, Monoid m) => (QName -> m) -> a -> m
- metasIn :: (NamesIn a, Collection MetaId m) => a -> m
- metasIn' :: (NamesIn a, Monoid m) => (MetaId -> m) -> a -> m
- namesAndMetasIn :: (NamesIn a, Collection QName m1, Collection MetaId m2) => a -> (m1, m2)
- class NamesIn a where
  - namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> a -> m
- newtype PSyn = PSyn PatternSynDefn

# Documentation

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

Some or all of the `QName`s that can be found in the given thing.

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

Some or all of the `QName`s that can be found in the given thing.

metasIn :: (NamesIn a, Collection MetaId m) => a -> m Source #

Some or all of the meta-variables that can be found in the given thing.

metasIn' :: (NamesIn a, Monoid m) => (MetaId -> m) -> a -> m Source #

Some or all of the meta-variables that can be found in the given thing.

namesAndMetasIn :: (NamesIn a, Collection QName m1, Collection MetaId m2) => a -> (m1, m2) Source #

Some or all of the names and meta-variables that can be found in the given thing.

class NamesIn a where Source #

Minimal complete definition

Nothing

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> a -> m Source #

Some or all of the names and meta-variables that can be found in the given thing.

default namesAndMetasIn' :: forall m (f :: Type -> Type) b. (Monoid m, Foldable f, NamesIn b, f b ~ a) => (Either QName MetaId -> m) -> a -> m Source #

#### Instances

Instances details

NamesIn AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> AmbiguousQName -> m Source #
NamesIn QName Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> QName -> m Source #
NamesIn MetaId Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> MetaId -> m Source #
NamesIn Clause Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Clause -> m Source #
NamesIn ConHead Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> ConHead -> m Source #
NamesIn ConPatternInfo Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> ConPatternInfo -> m Source #
NamesIn Level Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Level -> m Source #
NamesIn PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> PlusLevel -> m Source #
NamesIn Sort Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Sort -> m Source #
NamesIn Term Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Term -> m Source #
NamesIn PSyn Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> PSyn -> m Source #
NamesIn Literal Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Literal -> m Source #
NamesIn CaseInfo Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CaseInfo -> m Source #
NamesIn CaseType Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CaseType -> m Source #
NamesIn Compiled Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Compiled -> m Source #
NamesIn TAlt Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> TAlt -> m Source #
NamesIn TTerm Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> TTerm -> m Source #
NamesIn CompiledClauses Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CompiledClauses -> m Source #
NamesIn CompKit Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CompKit -> m Source #
NamesIn Definition Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Definition -> m Source #
NamesIn Defn Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Defn -> m Source #
NamesIn DisplayForm Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> DisplayForm -> m Source #
NamesIn DisplayTerm Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> DisplayTerm -> m Source #
NamesIn ExtLamInfo Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> ExtLamInfo -> m Source #
NamesIn NLPSort Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> NLPSort -> m Source #
NamesIn NLPType Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> NLPType -> m Source #
NamesIn NLPat Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> NLPat -> m Source #
NamesIn PrimFun Source # | Note that the `primFunImplementation` is skipped.
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> PrimFun -> m Source #
NamesIn RewriteRule Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> RewriteRule -> m Source #
NamesIn Section Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Section -> m Source #
NamesIn System Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> System -> m Source #
NamesIn Bool Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Bool -> m Source #
NamesIn (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Pattern' a -> m Source #
NamesIn a => NamesIn (Arg a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Arg a -> m Source #
NamesIn a => NamesIn (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> FieldAssignment' a -> m Source #
NamesIn a => NamesIn (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Abs a -> m Source #
NamesIn (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Pattern' a -> m Source #
NamesIn a => NamesIn (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Substitution' a -> m Source #
NamesIn a => NamesIn (Tele a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Tele a -> m Source #
NamesIn a => NamesIn (Type' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Type' a -> m Source #
NamesIn a => NamesIn (Elim' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Elim' a -> m Source #
NamesIn a => NamesIn (Case a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Case a -> m Source #
NamesIn a => NamesIn (WithArity a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> WithArity a -> m Source #
NamesIn a => NamesIn (Builtin a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Builtin a -> m Source #
NamesIn a => NamesIn (FunctionInverse' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> FunctionInverse' a -> m Source #
NamesIn a => NamesIn (Open a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Open a -> m Source #
NamesIn a => NamesIn (List1 a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> List1 a -> m Source #
NamesIn a => NamesIn (Set a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Set a -> m Source #
NamesIn a => NamesIn (Maybe a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Maybe a -> m Source #
NamesIn a => NamesIn (Maybe a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Maybe a -> m Source #
NamesIn a => NamesIn [a] Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> [a] -> m Source #
NamesIn a => NamesIn (Named n a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Named n a -> m Source #
(NamesIn a, NamesIn b) => NamesIn (Dom' a b) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Dom' a b -> m Source #
NamesIn a => NamesIn (Map k a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Map k a -> m Source #
(NamesIn a, NamesIn b) => NamesIn (HashMap a b) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> HashMap a b -> m Source #
(NamesIn a, NamesIn b) => NamesIn (a, b) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> 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 namesAndMetasIn' :: Monoid m => (Either QName MetaId -> 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 namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> (a, b, c, d) -> m Source #
(NamesIn a, NamesIn b, NamesIn c, NamesIn d, NamesIn e) => NamesIn (a, b, c, d, e) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> (a, b, c, d, e) -> m Source #
(NamesIn a, NamesIn b, NamesIn c, NamesIn d, NamesIn e, NamesIn f) => NamesIn (a, b, c, d, e, f) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> (a, b, c, d, e, f) -> m Source #

newtype PSyn Source #

Constructors

PSyn PatternSynDefn |

#### Instances

Instances details

NamesIn PSyn Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> PSyn -> m Source #