| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Rules.Data

Contents

Datatypes

Synopsis

checkDataDef :: DefInfo -> Induction -> QName -> [LamBinding] -> [Constructor] -> TCM ()
checkConstructor :: QName -> Telescope -> Nat -> Sort -> Induction -> Constructor -> TCM ()
bindParameters :: [LamBinding] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
fitsIn :: Type -> Sort -> TCM ()
constructs :: Int -> Type -> QName -> TCM ()
forceData :: MonadTCM tcm => QName -> Type -> tcm Type
isCoinductive :: MonadTCM tcm => Type -> tcm (Maybe Bool)

Datatypes

checkDataDef :: DefInfo -> Induction -> QName -> [LamBinding] -> [Constructor] -> TCM () | Source

Type check a datatype definition. Assumes that the type has already been checked.

checkConstructor | Source

:: QName |
-> Telescope |
-> Nat |
-> Sort |
-> Induction | Is the constructor inductive or coinductive?
-> Constructor |
-> TCM () |
Type check a constructor declaration. Checks that the constructor targets the datatype and that it fits inside the declared sort.

bindParameters :: [LamBinding] -> Type -> (Telescope -> Type -> TCM a) -> TCM a | Source

Bind the parameters of a datatype. The bindings should be domain free.

fitsIn :: Type -> Sort -> TCM () | Source

Check that the arguments to a constructor fits inside the sort of the datatype. The first argument is the type of the constructor.

constructs :: Int -> Type -> QName -> TCM () | Source

Check that a type constructs something of the given datatype. The first argument is the number of parameters to the datatype. TODO: what if there's a meta here?

forceData :: MonadTCM tcm => QName -> Type -> tcm Type | Source

Force a type to be a specific datatype.

isCoinductive :: MonadTCM tcm => Type -> tcm (Maybe Bool) | Source

Is the type coinductive? Returns `Nothing` if the answer cannot be determined.
Produced by Haddock version 2.4.2