|
Agda.TypeChecking.Records |
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
Order the fields of a record construction.
Use the second argument for missing fields.
|
|
|
The name of the module corresponding to a record.
|
|
|
Get the definition for a record. Throws an exception if the name
does not refer to a record.
|
|
|
Get the field names of a record.
|
|
|
Get the field types of a record.
|
|
|
Get the type of the record constructor.
|
|
|
Returns the given record type's constructor name (with an empty
range).
|
|
|
Check if a name refers to a record.
|
|
|
Compute the eta expansion of a record. The first argument should be
the name of a record type. Given
record R : Set where x : A; y : B and r : R, etaExpand R [] r is [R.x r, R.y r]
|
|
|
The fields should be eta contracted already.
|
|
Produced by Haddock version 2.6.0 |