Commit 84dd0dc5 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

fix the pretty-printing of custom reals in TPTP

parent 9ed1be10
......@@ -96,7 +96,9 @@ let number_format = {
Number.dec_real_support = Number.Number_default;
Number.hex_real_support = Number.Number_unsupported;
Number.frac_real_support = Number.Number_custom
(Number.PrintFracReal ("%s", "(%s * %s)", "(%s / %s)"));
(Number.PrintFracReal ("$to_real(%s)",
"$product($to_real(%s),$to_real(%s))",
"$quotient($to_real(%s),$to_real(%s))"));
Number.def_real_support = Number.Number_unsupported;
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment