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.6.0