Agda.Syntax.Internal.MetaVars

Documentation

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

Returns every meta-variable occurrence in the given type, except for those in Sorts.

allMetasList :: TermLike 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.

noMetas :: TermLike a => a -> Bool

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

firstMeta :: TermLike a => a -> Maybe MetaId

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