Agda.TypeChecking.Datatypes

Constructors

getConHead :: QName -> TCM ConHead

Get true constructor with record fields.

getConTerm :: QName -> TCM Term

Get true constructor as term.

getConForm :: QName -> TCM ConHead

Get true constructor with fields, expanding literals to constructors if possible.

getOrigConHead :: QName -> TCM ConHead

Augment constructor with record fields (preserve constructor name). The true constructor might only surface via reduce.

getOrigConTerm :: QName -> TCM Term

Analogous to getConTerm.

getConstructorData :: HasConstInfo m => QName -> m QName

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

getConType :: ConHead -> Type -> TCM (Maybe Type)

getConType c t computes the constructor parameters from type t and returns the instantiated type of constructor c. Nothing if t is not a data/record type or does not have a constructor c. Precondition: t is reduced.

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

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.

Data types

isDatatype :: QName -> TCM Bool

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

data DataOrRecord

Constructors

IsData

IsRecord

Instances

Eq DataOrRecord

Ord DataOrRecord

Show DataOrRecord

isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)

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

isDataOrRecord :: Term -> TCM (Maybe QName)

Precodition: Term is reduced.

getNumberOfParameters :: QName -> TCM (Maybe Nat)