Agda.TypeChecking.Datatypes
- getConstructorData :: MonadTCM tcm => QName -> tcm QName
- isDatatype :: MonadTCM tcm => QName -> tcm Bool
- data DatatypeInfo = DataInfo {}
- getDatatypeInfo :: MonadTCM tcm => Type -> tcm (Maybe DatatypeInfo)
Documentation
getConstructorData :: MonadTCM tcm => QName -> tcm QName
Get the name of the datatype constructed by a given constructor. Precondition: The argument must refer to a constructor
isDatatype :: MonadTCM tcm => QName -> tcm Bool
Check if a name refers to a datatype or a record with a named constructor.
data DatatypeInfo
Constructors
DataInfo | |
Fields
|
getDatatypeInfo :: MonadTCM tcm => Type -> tcm (Maybe DatatypeInfo)
Get the name and parameters from a type if it's a datatype or record type with a named constructor.