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