| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Records

Synopsis

orderFields :: MonadTCM tcm => QName -> a -> [Name] -> [(Name, a)] -> tcm [a]
recordModule :: QName -> ModuleName
getRecordDef :: MonadTCM tcm => QName -> tcm Defn
getRecordFieldNames :: MonadTCM tcm => QName -> tcm [(Hiding, Name)]
getRecordFieldTypes :: MonadTCM tcm => QName -> tcm Telescope
getRecordConstructorType :: MonadTCM tcm => QName -> tcm Type
getRecordConstructor :: MonadTCM tcm => QName -> tcm QName
isRecord :: MonadTCM tcm => QName -> tcm Bool
etaExpandRecord :: MonadTCM tcm => QName -> Args -> Term -> tcm (Telescope, Args)
etaContractRecord :: MonadTCM tcm => QName -> Args -> tcm Term

Documentation

orderFields :: MonadTCM tcm => QName -> a -> [Name] -> [(Name, a)] -> tcm [a] | Source

Order the fields of a record construction. Use the second argument for missing fields.

recordModule :: QName -> ModuleName | Source

The name of the module corresponding to a record.

getRecordDef :: MonadTCM tcm => QName -> tcm Defn | Source

Get the definition for a record. Throws an exception if the name does not refer to a record.

getRecordFieldNames :: MonadTCM tcm => QName -> tcm [(Hiding, Name)] | Source

Get the field names of a record.

getRecordFieldTypes :: MonadTCM tcm => QName -> tcm Telescope | Source

Get the field types of a record.

getRecordConstructorType :: MonadTCM tcm => QName -> tcm Type | Source

Get the type of the record constructor.

getRecordConstructor :: MonadTCM tcm => QName -> tcm QName | Source

Returns the given record type's constructor name (with an empty range).

isRecord :: MonadTCM tcm => QName -> tcm Bool | Source

Check if a name refers to a record.

etaExpandRecord :: MonadTCM tcm => QName -> Args -> Term -> tcm (Telescope, Args) | Source

Compute the eta expansion of a record. The first argument should be the name of a record type. Given

    record R : Set where x : A; y : B

and `r : R`, `etaExpand R [] r` is `[R.x r, R.y r]`

etaContractRecord :: MonadTCM tcm => QName -> Args -> tcm Term | Source

The fields should be eta contracted already.
Produced by Haddock version 2.4.2