Agda- A dependently typed functional programming language and proof assistant

Safe HaskellSafe-Infered




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.

getRecordFieldNames :: QName -> TCM [Arg Name]Source

Get the field names of 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).

isRecord :: QName -> TCM BoolSource

Check if a name refers to a record.

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.

isSingletonRecord :: 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.