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

Safe HaskellNone
LanguageHaskell98

Agda.Syntax.Internal.Defs

Description

Extract used definitions from terms.

Synopsis

Documentation

getDefs' :: (GetDefs a, Monoid b) => (MetaId -> Maybe Term) -> (QName -> b) -> a -> b 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 [QName] or Set QName. Note that emb can also choose to discard a used definition by mapping to the unit of the monoid.

type GetDefsM b = ReaderT (GetDefsEnv b) (Writer b) Source

Inputs to and outputs of getDefs' are organized as a monad.

data GetDefsEnv b Source

Constructors

GetDefsEnv 

Fields

lookupMeta :: MetaId -> Maybe Term
 
embDef :: QName -> b
 

Instances

class Monad m => MonadGetDefs m where Source

What it takes to get the used definitions.

Methods

doDef :: QName -> m () Source

doMeta :: MetaId -> m () Source

Instances