- 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.
:: 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 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.