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

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

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

datatypeName :: QName
datatypeParTel :: Telescope
datatypePars :: Args
datatypeIxTel :: Telescope
datatypeIxs :: Args

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.