- checkRecDef :: DefInfo -> QName -> Maybe Constructor -> [LamBinding] -> Expr -> [Constructor] -> TCM ()
- checkRecordProjections :: ModuleName -> QName -> Telescope -> Telescope -> [Declaration] -> TCM ()
Records
checkRecDef :: DefInfo -> QName -> Maybe Constructor -> [LamBinding] -> Expr -> [Constructor] -> TCM ()Source
checkRecordProjections :: ModuleName -> QName -> Telescope -> Telescope -> [Declaration] -> TCM ()Source
checkRecordProjections q tel ftel s vs n fs
:
m
: name of the generated module
q
: name of the record
tel
: parameters
s
: sort of the record
ftel
: telescope of fields
vs
: values of previous fields (should have one free variable, which is
the record)
fs
: the fields to be checked