Safe Haskell | Safe-Infered |
---|
- orderFields :: QName -> a -> [Name] -> [(Name, a)] -> TCM [a]
- recordModule :: QName -> ModuleName
- getRecordDef :: QName -> TCM Defn
- getRecordFieldNames :: QName -> TCM [Arg Name]
- findPossibleRecords :: [Name] -> TCM [QName]
- getRecordFieldTypes :: QName -> TCM Telescope
- getRecordConstructorType :: QName -> TCM Type
- getRecordConstructor :: QName -> TCM QName
- isRecord :: QName -> TCM Bool
- isEtaRecord :: QName -> TCM Bool
- isEtaRecordType :: Type -> TCM (Maybe (QName, Args))
- isRecordConstructor :: QName -> TCM Bool
- isGeneratedRecordConstructor :: QName -> TCM Bool
- etaExpandRecord :: QName -> Args -> Term -> TCM (Telescope, Args)
- etaContractRecord :: QName -> QName -> Args -> TCM Term
- isSingletonRecord :: QName -> Args -> TCM (Either MetaId Bool)
- isSingletonRecordModuloRelevance :: QName -> Args -> TCM (Either MetaId Bool)
- isSingletonRecord' :: Bool -> QName -> Args -> TCM (Either MetaId Bool)
Documentation
orderFields :: 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 :: QName -> TCM DefnSource
Get the definition for a record. Throws an exception if the name does not refer to a record.
findPossibleRecords :: [Name] -> TCM [QName]Source
Find all records with at least the given fields.
getRecordFieldTypes :: QName -> TCM TelescopeSource
Get the field types of a record.
getRecordConstructorType :: QName -> TCM TypeSource
Get the type of the record constructor.
getRecordConstructor :: QName -> TCM QNameSource
Returns the given record type's constructor name (with an empty range).
isEtaRecord :: QName -> TCM BoolSource
Check if a name refers to an eta expandable record.
isEtaRecordType :: Type -> TCM (Maybe (QName, Args))Source
Check if a type is an eta expandable record and return the record identifier and the parameters.
isRecordConstructor :: QName -> TCM BoolSource
Check if a name refers to a record constructor.
isGeneratedRecordConstructor :: QName -> TCM BoolSource
Check if a constructor name is the internally generated record constructor.
etaExpandRecord :: 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 :: QName -> QName -> Args -> TCM TermSource
The fields should be eta contracted already.