Agda-2.2.10: A dependently typed functional programming language and proof assistant Source code Contents Index

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 QName Source

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 Source

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