Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Rules.Record

Contents

Synopsis

Records

checkRecDef Source #

Arguments

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

addCompositionForRecord Source #

Arguments

:: QName

Datatype name.

-> EtaEquality 
-> ConHead 
-> Telescope

Γ parameters.

-> [Arg QName]

Projection names.

-> Telescope

Γ ⊢ Φ field types.

-> Type

Γ ⊢ T target type.

-> TCM () 

defineCompKitR Source #

Arguments

:: QName

some name, e.g. record name

-> Telescope

param types Δ

-> Telescope

fields' types Δ ⊢ Φ

-> [Arg QName]

fields' names

-> Type

record type Δ ⊢ T

-> TCM CompKit 

defineKanOperationR Source #

Arguments

:: 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) 

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

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