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





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

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

checkConstructor :: QName -> Telescope -> Nat -> Sort -> Constructor -> TCM ()Source

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.