Agda.Syntax.Internal.MetaVars · Agda-2.8.0.2

classclass AllMetas t where

#

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

Methods

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

Instances20AllMetas, …

AllMetas LevelDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars
AllMetas PlusLevelDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars
AllMetas SortDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars
AllMetas TermDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars
AllMetas TypeDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars
AllMetas CompareAsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
AllMetas ConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
AllMetas NLPSortDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
AllMetas NLPTypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
AllMetas NLPatDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
AllMetas StringDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars
TermLike a => AllMetas (Tele a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars
TermLike a => AllMetas (Elim' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars
AllMetas a => AllMetas (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars
AllMetas a => AllMetas (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars
AllMetas a => AllMetas [a]Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars
(AllMetas a, AllMetas b) => AllMetas (Dom' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars
(AllMetas a, AllMetas b) => AllMetas (a, b)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars
(AllMetas a, AllMetas b, AllMetas c) => AllMetas (a, b, c)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars
(AllMetas a, AllMetas b, AllMetas c, AllMetas d) => AllMetas (a, b, c, d)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars

valueallMetas' :: (TermLike a, Monoid m) => (MetaId -> m) -> a -> m

#

valueallMetasList :: AllMetas a => a -> [MetaId]

#

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.

valuenoMetas :: AllMetas a => a -> Bool

#

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

valuefirstMeta :: AllMetas a => a -> Maybe MetaId

#

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

valueunblockOnAnyMetaIn :: AllMetas t => t -> Blocker

#

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

valueunblockOnAllMetasIn :: AllMetas t => t -> Blocker

#

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