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

Agda.TypeChecking.Datatypes

Synopsis

Documentation

getConstructorData :: QName -> TCM QNameSource

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

isDatatype :: QName -> TCM BoolSource

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

isDataOrRecordType :: QName -> TCM BoolSource

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

getDatatypeInfo :: 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.