| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Rules.Record
Contents
Synopsis
- checkRecDef :: DefInfo -> QName -> UniverseCheck -> RecordDirectives -> DataDefParams -> Expr -> [Field] -> TCM ()
- addCompositionForRecord :: QName -> EtaEquality -> ConHead -> Telescope -> [Arg QName] -> Telescope -> Type -> TCM ()
- defineCompKitR :: QName -> Telescope -> Telescope -> [Arg QName] -> Type -> TCM CompKit
- defineKanOperationR :: Command -> QName -> Telescope -> Telescope -> [Arg QName] -> Type -> TCM (Maybe QName)
- checkRecordProjections :: ModuleName -> QName -> Bool -> ConHead -> Telescope -> Telescope -> [Declaration] -> TCM ()
Records
Arguments
| :: DefInfo | Position and other info. |
| -> QName | Record type identifier. |
| -> UniverseCheck | Check universes? |
| -> RecordDirectives | (Co)Inductive, (No)Eta, (Co)Pattern, Constructor? |
| -> DataDefParams | Record parameters. |
| -> Expr | Approximate type of constructor ( |
| -> [Field] | Field signatures. |
| -> TCM () |
checkRecDef i name con ps contel fields
name- Record type identifier.
con- Maybe constructor name and info.
ps- Record parameters.
contel- Approximate type of constructor (
fields-> dummy). Does not include record parameters. fields- List of field signatures.
checkRecordProjections :: ModuleName -> QName -> Bool -> ConHead -> Telescope -> Telescope -> [Declaration] -> TCM () Source #
checkRecordProjections m r q tel ftel fs.
m- name of the generated module
r- name of the record type
con- name of the record constructor
tel- parameters (perhaps erased) and record variable r ("self")
ftel- telescope of fields
fs- the fields to be checked