Agda-2.6.0.1: 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 -> Maybe (Ranged Induction) -> Maybe HasEta -> Maybe QName -> DataDefParams -> Expr -> [Field] -> TCM ()
- addCompositionForRecord :: QName -> ConHead -> Telescope -> [Arg QName] -> Telescope -> Type -> TCM ()
- defineCompKitR :: QName -> Telescope -> Telescope -> [Arg QName] -> Type -> TCM CompKit
- defineTranspOrHCompR :: TranspOrHComp -> 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?
-> Maybe (Ranged Induction) | Optional: (co)inductive declaration.
-> Maybe HasEta | Optional: user specified eta/no-eta
-> Maybe QName | Optional: constructor name.
-> DataDefParams | Record parameters.
-> Expr | Approximate type of constructor (`fields` -> Set). 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` -> Set). Does not include record parameters.
`fields`
  List of field signatures.

addCompositionForRecord :: QName -> ConHead -> Telescope -> [Arg QName] -> Telescope -> Type -> TCM () Source #

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 |

defineTranspOrHCompR Source #

Arguments

:: TranspOrHComp |
-> 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 and record variable r ("self")
`ftel`
  telescope of fields
`fs`
  the fields to be checked