Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Internal.Defs

Description

Extract used definitions from terms.

Synopsis

getDefListNoMetas :: Term -> [QName]
class GetDefs a where
- getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> a -> m

Documentation

getDefListNoMetas :: Term -> [QName] Source #

Get list of definitions, throw an error if any metavariable is encountered.

class GetDefs a where Source #

Getting the used definitions.

Note: in contrast to foldTerm getDefs also collects from sorts in terms. Thus, this is not an instance of foldTerm.

Methods

getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> a -> m Source #

getDefs lookup emb a extracts all used definitions (functions, data/record types) from a, embedded into a monoid via emb. Instantiations of meta variables are obtained via lookup.

Typical monoid instances would be Endo [QName] or Set QName. Do not use [QName] because of obvious quadratic slowdown. Note that emb can also choose to discard a used definition by mapping to the unit of the monoid.

Instances

Instances details

GetDefs MetaId Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> MetaId -> m Source #
GetDefs Clause Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> Clause -> m Source #
GetDefs Level Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> Level -> m Source #
GetDefs PlusLevel Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> PlusLevel -> m Source #
GetDefs Sort Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> Sort -> m Source #
GetDefs Telescope Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> Telescope -> m Source #
GetDefs Term Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> Term -> m Source #
GetDefs Type Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> Type -> m Source #
GetDefs String Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> String -> m Source #
GetDefs a => GetDefs (Arg a) Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> Arg a -> m Source #
GetDefs a => GetDefs (Abs a) Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> Abs a -> m Source #
GetDefs a => GetDefs (Dom a) Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> Dom a -> m Source #
GetDefs a => GetDefs (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> Elim' a -> m Source #
GetDefs a => GetDefs (Maybe a) Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> Maybe a -> m Source #
GetDefs a => GetDefs [a] Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> [a] -> m Source #
(GetDefs a, GetDefs b) => GetDefs (a, b) Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> (a, b) -> m Source #