- 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 -> 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 [(Hiding, 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).