Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 [Arg 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
isEtaRecord :: MonadTCM tcm => QName -> tcm Bool
isRecordConstructor :: MonadTCM tcm => QName -> tcm Bool
isGeneratedRecordConstructor :: MonadTCM tcm => QName -> tcm Bool
etaExpandRecord :: MonadTCM tcm => QName -> Args -> Term -> tcm (Telescope, Args)
etaContractRecord :: MonadTCM tcm => QName -> QName -> Args -> tcm Term
isSingletonRecord :: MonadTCM tcm => QName -> Args -> tcm (Either MetaId Bool)
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 -> ModuleNameSource
The name of the module corresponding to a record.
getRecordDef :: MonadTCM tcm => QName -> tcm DefnSource
Get the definition for a record. Throws an exception if the name does not refer to a record.
getRecordFieldNames :: MonadTCM tcm => QName -> tcm [Arg Name]Source
Get the field names of a record.
getRecordFieldTypes :: MonadTCM tcm => QName -> tcm TelescopeSource
Get the field types of a record.
getRecordConstructorType :: MonadTCM tcm => QName -> tcm TypeSource
Get the type of the record constructor.
getRecordConstructor :: MonadTCM tcm => QName -> tcm QNameSource
Returns the given record type's constructor name (with an empty range).
isRecord :: MonadTCM tcm => QName -> tcm BoolSource
Check if a name refers to a record.
isEtaRecord :: MonadTCM tcm => QName -> tcm BoolSource
Check if a name refers to an eta expandable record.
isRecordConstructor :: MonadTCM tcm => QName -> tcm BoolSource
Check if a name refers to a record constructor.
isGeneratedRecordConstructor :: MonadTCM tcm => QName -> tcm BoolSource
Check if a constructor name is the internally generated record constructor.
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; .z : C

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

etaContractRecord :: MonadTCM tcm => QName -> QName -> Args -> tcm TermSource
The fields should be eta contracted already.
isSingletonRecord :: MonadTCM tcm => QName -> Args -> tcm (Either MetaId Bool)Source

Is the type a hereditarily singleton record type? May return a blocking metavariable.

Precondition: The name should refer to a record type, and the arguments should be the parameters to the type.

Produced by Haddock version 2.6.1