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

Safe HaskellNone

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

getConstructorArity :: QName -> TCM (Either Nat [Arg QName])Source

Return the number of non-parameter arguments to a data constructor, or the field names of a record constructor.

For getting just the arity of constructor c, use either id size $ getConstructorArity c.

isDatatype :: QName -> TCM BoolSource

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

isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)Source

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