Agda-2.6.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 Source #

Arguments

:: QName	Datatype name.
-> 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

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