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

Safe Haskell | Safe-Infered

Agda.TypeChecking.Datatypes

Synopsis

- getConstructorData :: QName -> TCM QName
- isDatatype :: QName -> TCM Bool
- isDataOrRecordType :: QName -> TCM Bool
- data DatatypeInfo = DataInfo {
  - datatypeName :: QName
  - datatypeParTel :: Telescope
  - datatypePars :: Args
  - datatypeIxTel :: Telescope
  - datatypeIxs :: Args
  }
- getDatatypeInfo :: Type -> TCM (Maybe DatatypeInfo)

# Documentation

getConstructorData :: QName -> TCM QName

Get the name of the datatype constructed by a given constructor. Precondition: The argument must refer to a constructor

isDatatype :: QName -> TCM Bool

Check if a name refers to a datatype or a record with a named constructor.

isDataOrRecordType :: QName -> TCM Bool

Check if a name refers to a datatype or a record.

data DatatypeInfo

Constructors

DataInfo |
Fields datatypeName :: QName datatypeParTel :: Telescope datatypePars :: Args datatypeIxTel :: Telescope datatypeIxs :: Args

getDatatypeInfo :: Type -> TCM (Maybe DatatypeInfo)

Get the name and parameters from a type if it's a datatype or record type with a named constructor.