max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: more unit tests

Browse source 
Some taken from https://stackoverflow.com/questions/37172819/test-if-c98-string-is-a-number-in-scientific-notation
This commit is contained in:
E.W.Ayers 2022-08-17 10:05:09 +01:00 • committed by Leonardo de Moura
parent 4e7c1e1ec8
commit 81ad807bb3
2 changed files with 53 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
tests/lean/scientific.lean
View file

@ -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

32
tests/lean/scientific.lean.expected.out
View file

@ -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