:: ModuleName	Name of new module defined by the module macro.
-> Telescope	Parameters of new module.
-> ModuleName	Name of old module applied to arguments.
-> Args	Arguments of module application.
-> Map QName QName	Imported names (given as renaming).
-> Map ModuleName ModuleName	Imported modules (given as renaming).
-> TCM ()

Module application (followed by module parameter abstraction).

addDisplayForm :: QName -> DisplayForm -> TCM () Source

canonicalName :: QName -> TCM QName Source

sameDef :: QName -> QName -> TCM (Maybe QName) Source

whatInduction :: QName -> TCM Induction Source

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

singleConstructorType :: QName -> TCM Bool Source

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

Precondition: The name has to refer to a constructor.

class (Functor m, Applicative m, Monad m) => HasConstInfo m where Source

Methods

getConstInfo :: QName -> m Definition Source

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

Instances

HasConstInfo ReduceM
HasConstInfo Unify
HasConstInfo (TCMT IO)

getConInfo :: MonadTCM tcm => ConHead -> tcm Definition Source

getPolarity :: QName -> TCM [Polarity] Source

Look up the polarity of a definition.

getPolarity' :: Comparison -> QName -> TCM [Polarity] Source

Look up polarity of a definition and compose with polarity represented by Comparison.

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

Set the polarity of a definition.

getArgOccurrences :: QName -> TCM [Occurrence] Source

Return a finite list of argument occurrences.

getArgOccurrence :: QName -> Nat -> TCM Occurrence Source

setArgOccurrences :: QName -> [Occurrence] -> TCM () Source

getMutual :: QName -> TCM [QName] Source

Get the mutually recursive identifiers.

setMutual :: QName -> [QName] -> TCM () Source

Set the mutually recursive identifiers.

mutuallyRecursive :: QName -> QName -> TCM Bool Source

Check whether two definitions are mutually recursive.

getSecFreeVars :: ModuleName -> TCM Nat Source

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

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

getDefFreeVars :: QName -> TCM Nat Source

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

Compute the context variables to apply a definition to.

instantiateDef :: Definition -> TCM Definition Source

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

makeAbstract :: Definition -> Maybe Definition Source

Give the abstract view of a definition.

inAbstractMode :: TCM a -> TCM a Source

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

inConcreteMode :: TCM a -> TCM a Source

Not in abstract mode. All abstract definitions are opaque.

ignoreAbstractMode :: MonadReader TCEnv m => m a -> m a Source

Ignore abstract mode. All abstract definitions are transparent.

treatAbstractly :: MonadReader TCEnv m => QName -> m Bool Source

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.

treatAbstractly' :: QName -> TCEnv -> Bool Source

typeOfConst :: QName -> TCM Type Source

Get type of a constant, instantiated to the current context.

relOfConst :: QName -> TCM Relevance Source

Get relevance of a constant.

colOfConst :: QName -> TCM [Color] Source

Get colors of a constant.

sortOfConst :: QName -> TCM Sort Source

The name must be a datatype.

isProjection :: QName -> TCM (Maybe Projection) Source

Is it the name of a record projection?

isProjection_ :: Defn -> Maybe Projection Source

isProperProjection :: Defn -> Bool Source

projectionArgs :: Defn -> Int Source

Number of dropped initial arguments.

applyDef :: QName -> Arg Term -> TCM Term Source

Apply a function f to its first argument, producing the proper postfix projection if f is a projection.

getDefType :: QName -> Type -> TCM (Maybe Type) Source

getDefType f t computes the type of (possibly projection-(like)) function t whose first argument has type t. The parameters for f are extracted from t. Nothing if f is projection(like) but t is not a datarecordaxiom type.

Precondition: t is reduced.