Agda.Syntax.Internal.MetaVars

Documentation

class AllMetas t where

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

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

Instances

AllMetas PlusLevel

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Level

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Sort

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Type

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Term

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas CompareAs

Defined in Agda.TypeChecking.Monad.Base

Methods

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

AllMetas Constraint

Defined in Agda.TypeChecking.Monad.Base

Methods

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

AllMetas a => AllMetas [a]

Defined in Agda.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> [a] -> m

AllMetas a => AllMetas (Maybe a)

Defined in Agda.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> Maybe a -> m

AllMetas a => AllMetas (Arg a)

Defined in Agda.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> Arg a -> m

TermLike a => AllMetas (Elim' a)

Defined in Agda.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> Elim' a -> m

TermLike a => AllMetas (Tele a)

Defined in Agda.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> Tele a -> m

TermLike a => AllMetas (Dom a)

Defined in Agda.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> Dom a -> m

(AllMetas a, AllMetas b) => AllMetas (a, b)

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

(AllMetas a, AllMetas b, AllMetas c) => AllMetas (a, b, c)

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

(AllMetas a, AllMetas b, AllMetas c, AllMetas d) => AllMetas (a, b, c, d)

Defined in Agda.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> (a, b, c, d) -> m

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

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

noMetas :: AllMetas a => a -> Bool

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

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

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

unblockOnAnyMetaIn :: AllMetas t => t -> Blocker

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

unblockOnAllMetasIn :: AllMetas t => t -> Blocker

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