Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Datatypes
Synopsis
getConstructorData :: MonadTCM tcm => QName -> tcm QName
isDatatype :: MonadTCM tcm => QName -> tcm Bool
data DatatypeInfo = DataInfo {
datatypeName :: QName
datatypeParTel :: Telescope
datatypePars :: Args
datatypeIxTel :: Telescope
datatypeIxs :: Args
}
getDatatypeInfo :: MonadTCM tcm => Type -> tcm (Maybe DatatypeInfo)
Documentation
getConstructorData :: MonadTCM tcm => QName -> tcm QNameSource
Get the name of the datatype constructed by a given constructor. Precondition: The argument must refer to a constructor
isDatatype :: MonadTCM tcm => QName -> tcm BoolSource
Check if a name refers to a datatype or a record with a named constructor.
data DatatypeInfo Source
Constructors
DataInfo
datatypeName :: QName
datatypeParTel :: Telescope
datatypePars :: Args
datatypeIxTel :: Telescope
datatypeIxs :: Args
getDatatypeInfo :: MonadTCM tcm => Type -> tcm (Maybe DatatypeInfo)Source
Get the name and parameters from a type if it's a datatype or record type with a named constructor.
Produced by Haddock version 2.6.1