Unusual Float parsing

[eyelash]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The parsing of Float literals in Lean is somewhat unusual compared to other popular languages which might lead to unexpected behaviour.

Steps to Reproduce

#eval 1.0e   -- 1.000000
#eval 1.0e+1 -- 2.000000

Expected behavior:

1. I expect 1.0e to be an error. e should always have to be followed by a number.
2. I expect 1.0e+1 to parse as 10.0 just like it does in JavaScript, Java, C++, and Python.

Actual behavior: 1.0e is a valid Float literal and 1.0e+1 gets parsed as (1.0e) + (1) which is 2.0.

Reproduces how often: 100%

Versions

Lean v4.0.0-m5 (commit 7dbfaf9) on Ubuntu 20.04.