| Safe Haskell | None |
|---|
Agda.TypeChecking.Rules.Record
Contents
- checkRecDef :: DefInfo -> QName -> Maybe Induction -> Maybe QName -> [LamBinding] -> Expr -> [Field] -> TCM ()
- checkRecordProjections :: ModuleName -> QName -> QName -> Telescope -> Telescope -> [Declaration] -> TCM ()
Records
checkRecDef :: DefInfo -> QName -> Maybe Induction -> Maybe QName -> [LamBinding] -> Expr -> [Field] -> 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 and record variable r (self)
ftel- telescope of fields
fs- the fields to be checked