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




addConstant :: QName -> Definition -> TCM ()Source

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

makeProjection :: QName -> TCM ()Source

Turn a definition into a projection if it looks like a projection.

addSection :: ModuleName -> Nat -> TCM ()Source

Add a section to the signature.

lookupSection :: ModuleName -> TCM TelescopeSource

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

whatInduction :: 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 :: QName -> TCM [Polarity]Source

Look up the polarity of a definition.

setPolarity :: QName -> [Polarity] -> TCM ()Source

Set the polarity of a definition.

getSecFreeVars :: 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 :: ModuleName -> TCM NatSource

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

getDefFreeVars :: 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 :: QName -> TCM ArgsSource

Compute the context variables to apply a definition to.

instantiateDef :: 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 :: TCM a -> TCM aSource

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

inConcreteMode :: TCM a -> TCM aSource

Not in abstract mode. All abstract definitions are opaque.

ignoreAbstractMode :: TCM a -> TCM aSource

Ignore abstract mode. All abstract definitions are transparent.

treatAbstractly :: 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 :: QName -> TCM TypeSource

get type of a constant

relOfConst :: QName -> TCM RelevanceSource

get relevance of a constant

sortOfConst :: QName -> TCM SortSource

The name must be a datatype.

isProjection :: QName -> TCM (Maybe (QName, Int))Source

Is it the name of a record projection?