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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Syntax.Internal.MetaVars

Synopsis

- class AllMetas t where
  - allMetas :: Monoid m => (MetaId -> m) -> t -> m
- allMetas' :: (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
- allMetasList :: AllMetas a => a -> [MetaId]
- noMetas :: AllMetas a => a -> Bool
- firstMeta :: AllMetas a => a -> Maybe MetaId
- unblockOnAnyMetaIn :: AllMetas t => t -> Blocker
- unblockOnAllMetasIn :: AllMetas t => t -> Blocker

# Documentation

class AllMetas t where Source #

Returns every meta-variable occurrence in the given type, except for those in sort annotations on types.

Minimal complete definition

Nothing

Methods

allMetas :: Monoid m => (MetaId -> m) -> t -> m Source #

default allMetas :: (TermLike t, Monoid m) => (MetaId -> m) -> t -> m Source #

#### Instances

Instances details

AllMetas Level Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Level -> m Source #
AllMetas PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> PlusLevel -> m Source #
AllMetas Sort Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Sort -> m Source #
AllMetas Term Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Term -> m Source #
AllMetas Type Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Type -> m Source #
AllMetas CompareAs Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods allMetas :: Monoid m => (MetaId -> m) -> CompareAs -> m Source #
AllMetas Constraint Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods allMetas :: Monoid m => (MetaId -> m) -> Constraint -> m Source #
AllMetas a => AllMetas (Arg a) Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Arg a -> m Source #
TermLike a => AllMetas (Dom a) Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Dom a -> m Source #
TermLike a => AllMetas (Tele a) Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Tele a -> m Source #
TermLike a => AllMetas (Elim' a) Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Elim' a -> m Source #
AllMetas a => AllMetas (Maybe a) Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Maybe a -> m Source #
AllMetas a => AllMetas [a] Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> [a] -> m Source #
(AllMetas a, AllMetas b) => AllMetas (a, b) Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> (a, b) -> m Source #
(AllMetas a, AllMetas b, AllMetas c) => AllMetas (a, b, c) Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> (a, b, c) -> m Source #
(AllMetas a, AllMetas b, AllMetas c, AllMetas d) => AllMetas (a, b, c, d) Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> (a, b, c, d) -> m Source #

allMetas' :: (TermLike a, Monoid m) => (MetaId -> m) -> a -> m Source #

allMetasList :: AllMetas a => a -> [MetaId] Source #

Returns `allMetas` in a list. `allMetasList = allMetas (:[])`.

Note: this resulting list is computed via difference lists. Thus, use this function if you actually need the whole list of metas. Otherwise, use `allMetas` with a suitable monoid.

noMetas :: AllMetas a => a -> Bool Source #

`True` if thing contains no metas. `noMetas = null . allMetasList`.

firstMeta :: AllMetas a => a -> Maybe MetaId Source #

Returns the first meta it find in the thing, if any. `firstMeta == listToMaybe . allMetasList`.

unblockOnAnyMetaIn :: AllMetas t => t -> Blocker Source #

A blocker that unblocks if any of the metas in a term are solved.

unblockOnAllMetasIn :: AllMetas t => t -> Blocker Source #

A blocker that unblocks if any of the metas in a term are solved.