diff --git a/tests/lean/scientific.lean b/tests/lean/scientific.lean index c6eb415eb6..ada0b9c4a8 100644 --- a/tests/lean/scientific.lean +++ b/tests/lean/scientific.lean @@ -1,10 +1,28 @@ -- https://github.com/leanprover/lean4/issues/1484 -#eval 1.0e1 -- 10.000000 -#eval 1.0e+1 -- 10.000000 -#eval 1.0e-1 -- 0.1000000 +#eval 1.0e1 +#eval 1.0e+1 +#eval 1.0e-1 +#eval 1.453e-8 +#eval 0.05843E5 +#eval 8.43e6 +#eval 5.2342E-7 +#eval 123. +#eval 123.E+3 +#eval -853.4E-2 -#eval 1.0e -- error -#eval 1.0e+ -- error -#eval 1.0e- -- error -#eval 1.0e+ 1 -- error -#eval 1.0e + 1 -- error +-- we reject leading decimal points +#eval .123 +#eval .123E3 +#eval .123E00003 + +-- errors +#eval e-8 +#eval 1.0e +#eval 1.0e+ +#eval 1.0e- +#eval 1.0e+ 1 +#eval 1.0e + 1 +#eval 123E +#eval .E+03 +#eval -E3 +#eval 2e.2 diff --git a/tests/lean/scientific.lean.expected.out b/tests/lean/scientific.lean.expected.out index 1c76d1cdc6..28b77df7e3 100644 --- a/tests/lean/scientific.lean.expected.out +++ b/tests/lean/scientific.lean.expected.out @@ -1,8 +1,30 @@ 10.000000 10.000000 0.100000 -scientific.lean:6:9: error: missing exponent digits in scientific literal -scientific.lean:7:9: error: missing exponent digits in scientific literal -scientific.lean:8:9: error: missing exponent digits in scientific literal -scientific.lean:9:9: error: missing exponent digits in scientific literal -scientific.lean:10:9: error: missing exponent digits in scientific literal +0.000000 +5843.000000 +8430000.000000 +0.000001 +123.000000 +123000.000000 +-8.534000 +scientific.lean:14:6-14:7: error: invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`) +scientific.lean:14:7: error: expected command +scientific.lean:15:6-15:7: error: invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`) +scientific.lean:15:7: error: expected command +scientific.lean:16:6-16:7: error: invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`) +scientific.lean:16:7: error: expected command +scientific.lean:19:6-19:7: error: unknown identifier 'e' +scientific.lean:19:0-19:9: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors +scientific.lean:20:9: error: missing exponent digits in scientific literal +scientific.lean:21:9: error: missing exponent digits in scientific literal +scientific.lean:22:9: error: missing exponent digits in scientific literal +scientific.lean:23:9: error: missing exponent digits in scientific literal +scientific.lean:24:9: error: missing exponent digits in scientific literal +scientific.lean:25:9: error: missing exponent digits in scientific literal +scientific.lean:26:6-26:8: error: invalid dotted identifier notation, unknown identifier `Nat.E` from expected type + Nat +scientific.lean:26:0-26:11: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors +scientific.lean:27:7-27:9: error: unknown identifier 'E3' +scientific.lean:27:0-27:9: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors +scientific.lean:28:7: error: missing exponent digits in scientific literal