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.