kdrag.notation.Record

kdrag.notation.Record(name: str, *fields, pred=None) → DatatypeSortRef

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