Safe Haskell | None |
---|
- 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