| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Rules.Record
Contents
- checkRecDef :: DefInfo -> QName -> Maybe (Ranged Induction) -> Maybe QName -> [LamBinding] -> Expr -> [Field] -> TCM ()
- checkRecordProjections :: ModuleName -> QName -> ConHead -> Telescope -> Telescope -> [Declaration] -> TCM ()
Records
Arguments
| :: DefInfo | Position and other info. |
| -> QName | Record type identifier. |
| -> Maybe (Ranged Induction) | Optional: (co)inductive declaration. |
| -> Maybe QName | Optional: constructor name. |
| -> [LamBinding] | Record parameters. |
| -> Expr | Approximate type of constructor ( |
| -> [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-> Set). Does not include record parameters. fields- List of field signatures.
checkRecordProjections :: ModuleName -> QName -> 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 and record variable r ("self")
ftel- telescope of fields
fs- the fields to be checked