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

Safe Haskell | None

Agda.TypeChecking.Rules.Record

Contents

- Records

Synopsis

- checkRecDef :: DefInfo -> QName -> Maybe Induction -> Maybe QName -> [LamBinding] -> Expr -> [Field] -> TCM ()
- checkRecordProjections :: ModuleName -> QName -> QName -> Telescope -> Telescope -> [Declaration] -> TCM ()

# Records

checkRecDef :: DefInfo -> QName -> Maybe Induction -> Maybe QName -> [LamBinding] -> Expr -> [Field] -> 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).
`fields`
  List of field signatures.

checkRecordProjections :: ModuleName -> QName -> QName -> Telescope -> Telescope -> [Declaration] -> TCM ()

`checkRecordProjections m r q tel ftel fs`.

`m`
  name of the generated module
`r`
  name of the record type
`q`
  name of the record constructor
`tel`
  parameters and record variable r (self)
`ftel`
  telescope of fields
`fs`
  the fields to be checked