diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index 0b5fdf2f1..3a59961c6 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/lean_parser.cpp @@ -884,10 +884,14 @@ class parser::imp { } expr parse_decimal() { - not_implemented_yet(); + auto p = pos(); + expr r = save(mk_real_value(m_scanner.get_num_val()), p); + next(); + return r; } expr parse_string() { + // TODO not_implemented_yet(); } diff --git a/tests/lean/arith8.lean b/tests/lean/arith8.lean new file mode 100644 index 000000000..0accbcfe5 --- /dev/null +++ b/tests/lean/arith8.lean @@ -0,0 +1,5 @@ +Eval 10.3 +Eval 0.3 +Eval 0.3 + 0.1 +Eval 0.2 + 0.7 +Eval 1/3 + 0.1 \ No newline at end of file diff --git a/tests/lean/arith8.lean.expected.out b/tests/lean/arith8.lean.expected.out new file mode 100644 index 000000000..e69cc588d --- /dev/null +++ b/tests/lean/arith8.lean.expected.out @@ -0,0 +1,7 @@ + Set: pp::colors + Set: pp::unicode +103/10 +3/10 +2/5 +9/10 +13/30