Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Rules.Record

Contents

- Records

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

checkRecDef Source #

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 (`fields` -> dummy). Does not include record parameters.
-> [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.

addCompositionForRecord Source #

Arguments

:: QName | Datatype name.
-> EtaEquality |
-> ConHead |
-> Telescope | `Γ` parameters.
-> [Arg QName] | Projection names.
-> Telescope | `Γ ⊢ Φ` field types.
-> Type | `Γ ⊢ T` target type.
-> TCM () |

defineCompKitR Source #

Arguments

:: QName | some name, e.g. record name
-> Telescope | param types Δ
-> Telescope | fields' types Δ ⊢ Φ
-> [Arg QName] | fields' names
-> Type | record type Δ ⊢ T
-> TCM CompKit |

defineKanOperationR Source #

Arguments

:: Command |
-> QName | some name, e.g. record name
-> Telescope | param types Δ
-> Telescope | fields' types Δ ⊢ Φ
-> [Arg QName] | fields' names
-> Type | record type Δ ⊢ T
-> TCM (Maybe QName) |

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