# Generated by tools/translator: qualified upstream name -> MoonBit name.
define_auto_record_type define_auto_record_type
define_record_type define_record_type
get_record_components get_record_components
parse_record_specification parse_record_specification
record_extensionally_valid_component_thms record_extensionally_valid_component_thms
record_orthogonality_thms record_orthogonality_thms
record_read_write_thms record_read_write_thms
record_strongly_valid_component_thms record_strongly_valid_component_thms
record_valid_component_thms record_valid_component_thms
record_weakly_valid_component_thms record_weakly_valid_component_thms
the_record_types the_record_types
