# The Record Format Constructor

The special constructor `recformat< ... >` is used for the creation of record formats. A record format must be created before records in that format are created.

## `recformat< L >: FieldnameList -> RecFormat`

Construct the record format corresponding to the non-empty fieldname list $L$. Each term of $L$ must be one of the following:

**(a)**
$fieldname$ in which case there is no restriction on values that may be stored in this field of records having this format;

**(b)**
$fieldname {:}expression$ where the expression evaluates to a magma which will be the parent of values stored in this field of records having this format; or

**(c)**
$fieldname {:}expression$ where the expression evaluates to a category which will be the category of values stored in this field of records having this format;

where $fieldname$ consists of characters that would form a valid identifier name. Note that it is not a string.

## `Example: Record Format (ex-d1148b)`

We create a record format with these fields: `n`, an integer; `misc`, which has no restrictions; and `seq`, a sequence (with any universe possible).

```magma
> RF := recformat< n : Integers(), misc, seq : SeqEnum >;
> RF;
recformat<n: IntegerRing(), misc, seq: SeqEnum>
> Names(RF);
[ n, misc, seq ]

```
