rcf_num_to_string method
\brief Convert the RCF numeral into a string.
def_API('Z3_rcf_num_to_string', STRING, (_in(CONTEXT), _in(RCF_NUM), _in(BOOL), _in(BOOL)))
Implementation
Z3_string rcf_num_to_string(
Z3_context c,
Z3_rcf_num a,
bool compact,
bool html,
) {
return _rcf_num_to_string(
c,
a,
compact,
html,
);
}