Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Internal.MetaVars

Synopsis

Documentation

class AllMetas t where Source #

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 Source #

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

Instances

Instances details
AllMetas Level Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Sort Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Term Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Type Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

AllMetas Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

AllMetas a => AllMetas (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

TermLike a => AllMetas (Dom a) Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

TermLike a => AllMetas (Tele a) Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

TermLike a => AllMetas (Elim' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas a => AllMetas (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas a => AllMetas [a] Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

(AllMetas a, AllMetas b) => AllMetas (a, b) Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

(AllMetas a, AllMetas b, AllMetas c) => AllMetas (a, b, c) Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

(AllMetas a, AllMetas b, AllMetas c, AllMetas d) => AllMetas (a, b, c, d) Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

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

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