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

Safe Haskell | None

Agda.TypeChecking.Datatypes

Synopsis

- getConstructorData :: QName -> TCM QName
- getConstructorArity :: QName -> TCM (Either Nat [Arg QName])
- isDatatype :: QName -> TCM Bool
- data DataOrRecord
  - = IsData
  - | IsRecord
- 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

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)

getNumberOfParameters :: QName -> TCM (Maybe Nat)