Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- class AllMetas t where
- 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.
Nothing
Instances
allMetasList :: AllMetas a => a -> [MetaId] Source #
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.