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

Agda.TypeChecking.Monad.Signature

Synopsis

Documentation

withSignature :: MonadTCM tcm => Signature -> tcm a -> tcm aSource

addConstant :: MonadTCM tcm => QName -> Definition -> tcm ()Source

Add a constant to the signature. Lifts the definition to top level.

addSection :: MonadTCM tcm => ModuleName -> Nat -> tcm ()Source

Add a section to the signature.

lookupSection :: MonadTCM tcm => ModuleName -> tcm TelescopeSource

Lookup a section. If it doesn't exist that just means that the module wasn't parameterised.

whatInduction :: MonadTCM tcm => QName -> tcm InductionSource

Can be called on either a (co)datatype, a record type or a (co)constructor.

singleConstructorType :: QName -> TCM BoolSource

Does the given constructor come from a single-constructor type?

Precondition: The name has to refer to a constructor.

getConstInfo :: MonadTCM tcm => QName -> tcm DefinitionSource

Lookup the definition of a name. The result is a closed thing, all free variables have been abstracted over.

getPolarity :: MonadTCM tcm => QName -> tcm [Polarity]Source

Look up the polarity of a definition.

setPolarity :: MonadTCM tcm => QName -> [Polarity] -> tcm ()Source

Set the polarity of a definition.

getSecFreeVars :: MonadTCM tcm => ModuleName -> tcm NatSource

Look up the number of free variables of a section. This is equal to the number of parameters if we're currently inside the section and 0 otherwise.

getModuleFreeVars :: MonadTCM tcm => ModuleName -> tcm NatSource

Compute the number of free variables of a module. This is the sum of the free variables of its sections.

getDefFreeVars :: MonadTCM tcm => QName -> tcm NatSource

Compute the number of free variables of a defined name. This is the sum of the free variables of the sections it's contained in.

freeVarsToApply :: MonadTCM tcm => QName -> tcm ArgsSource

Compute the context variables to apply a definition to.

instantiateDef :: MonadTCM tcm => Definition -> tcm DefinitionSource

Instantiate a closed definition with the correct part of the current context.

makeAbstract :: Definition -> Maybe DefinitionSource

Give the abstract view of a definition.

inAbstractMode :: MonadTCM tcm => tcm a -> tcm aSource

Enter abstract mode. Abstract definition in the current module are transparent.

inConcreteMode :: MonadTCM tcm => tcm a -> tcm aSource

Not in abstract mode. All abstract definitions are opaque.

ignoreAbstractMode :: MonadTCM tcm => tcm a -> tcm aSource

Ignore abstract mode. All abstract definitions are transparent.

treatAbstractly :: MonadTCM tcm => QName -> tcm BoolSource

Check whether a name might have to be treated abstractly (either if we're inAbstractMode or it's not a local name). Returns true for things not declared abstract as well, but for those makeAbstract will have no effect.

typeOfConst :: MonadTCM tcm => QName -> tcm TypeSource

get type of a constant

relOfConst :: MonadTCM tcm => QName -> tcm RelevanceSource

get relevance of a constant

sortOfConst :: MonadTCM tcm => QName -> tcm SortSource

The name must be a datatype.

isProjection :: MonadTCM tcm => QName -> tcm (Maybe Int)Source

Is it the name of a record projection?