Skip to content

HORIZON HASKELL Docs lts/ghc-9.14.x3e2d5682026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 9.14.1 · lts/ghc-9.14.x · 3e2d568 · 2026-10-11

ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Rules.Record

5 values

PackageAgda-2.8.0.2
Exports5
LanguageHaskell2010
LicenceMIT
SourceRecord.hs

Records

5 declarations

valuecheckRecDef

:: DefInfo
Position and other info.
-> QName
Record type identifier.
-> UniverseCheck
Check universes?
-> RecordDirectives
(Co)Inductive, (No)Eta, (Co)Pattern, Constructor?
-> DataDefParams
Record parameters.
-> Expr
Approximate type of constructor (fields -> dummy). Does not include record parameters.
-> [Field]
Field signatures.
-> TCM ()

checkRecDef i name con ps contel fields

name

Record type identifier.

con

Maybe constructor name and info.

ps

Record parameters.

contel

Approximate type of constructor (

fields

-> dummy). Does not include record parameters.

fields

List of field signatures.

valueaddCompositionForRecord

:: QName
Datatype name.
-> EtaEquality
-> ConHead
-> Telescope
Γ parameters.
-> [Arg QName]
Projection names.
-> Telescope
Γ ⊢ Φ field types.
-> Type
Γ ⊢ T target type.
-> TCM ()

valuedefineCompKitR

:: QName
some name, e.g. record name
-> Telescope
param types Δ
-> Telescope
fields' types Δ ⊢ Φ
-> [Arg QName]
fields' names
-> Type
record type Δ ⊢ T
-> TCM CompKit

valuedefineKanOperationR

:: Command
-> QName
some name, e.g. record name
-> Telescope
param types Δ
-> Telescope
fields' types Δ ⊢ Φ
-> [Arg QName]
fields' names
-> Type
record type Δ ⊢ T
-> TCM (Maybe QName)

valuecheckRecordProjections

:: ModuleName
-> QName
-> Bool
-> ConHead
-> Telescope
-> Telescope
-> [Declaration]
-> TCM ()

checkRecordProjections m r q tel ftel fs.

m: name of the generated module
r: name of the record type
con: name of the record constructor
tel: parameters (perhaps erased) and record variable r ("self")
ftel: telescope of fields
fs: the fields to be checked