Safe Haskell | None |
---|
Agda.TypeChecking.Datatypes
- getConstructorData :: QName -> TCM QName
- getConstructorArity :: QName -> TCM (Either Nat [Arg QName])
- isDatatype :: QName -> TCM Bool
- data DataOrRecord
- isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)
- isDataOrRecord :: Term -> TCM (Maybe QName)
- getNumberOfParameters :: QName -> TCM (Maybe Nat)
Documentation
getConstructorData :: QName -> TCM QName
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])
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 Bool
Check if a name refers to a datatype or a record with a named constructor.
data DataOrRecord
Instances
isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)
Check if a name refers to a datatype or a record.
isDataOrRecord :: Term -> TCM (Maybe QName)
getNumberOfParameters :: QName -> TCM (Maybe Nat)