| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Rules.Record

Contents

Records

Synopsis

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
Produced by Haddock version 2.4.2