Agda-2.6.4.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 -> 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