Record()
Define a record datatype. The optional argument pred will add a well-formedness condition to the record giving something akin to a refinement type.