Agda-2.3.0: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Rules.Record

Contents

Synopsis

Records

checkRecDef :: DefInfo -> QName -> Maybe QName -> [LamBinding] -> Expr -> [Constructor] -> TCM ()Source

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 -> Set).
fields
List of field signatures.

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

checkRecordProjections m r q tel ftel fs.

m
name of the generated module
r
name of the record type
q
name of the record constructor
tel
parameters
ftel
telescope of fields
fs
the fields to be checked