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

Safe HaskellNone




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

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

allMetasList :: TermLike 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 :: TermLike a => a -> Bool Source #

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

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

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