Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone





getConHead :: QName -> TCM ConHead Source #

Get true constructor with record fields.

getConTerm :: QName -> TCM Term Source #

Get true constructor as term.

getConForm :: QName -> TCM ConHead Source #

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

getOrigConHead :: QName -> TCM ConHead Source #

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

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

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) Source #

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.

data HasEta Source #




Eq HasEta Source # 


(==) :: HasEta -> HasEta -> Bool #

(/=) :: HasEta -> HasEta -> Bool #

getConstructorInfo :: QName -> TCM ConstructorInfo 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.

Data types

isDatatype :: QName -> TCM Bool Source #

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.

isDataOrRecord :: Term -> TCM (Maybe QName) Source #

Precodition: Term is reduced.