Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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.
checkConstructorSource
:: QName
-> Telescope
-> Nat
-> Sort
-> InductionIs 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 aSource
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 TypeSource
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