Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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.6.0