diff --git a/tests/lean/decimals.lean b/tests/lean/decimals.lean index 26c0504b3f..9a7b4a46c7 100644 --- a/tests/lean/decimals.lean +++ b/tests/lean/decimals.lean @@ -14,3 +14,18 @@ theorem ex : 31416e-4 = 3.1416 := #eval 3.00e-100 * 1e100 #eval 3.00e-100 * 1.e100 #eval 3.00e-100 * 1.0e100 + +#eval 1e10 +#eval 1e50 +#eval 1e80 +#eval 1e100 +#eval 1e200 +#eval 1e300 +#eval 1e400 + +#eval 1 / 1e-1 +#eval 1 / 1e-2 +#eval 1 / 1e-10 +#eval 1 / 1e-100 +#eval 1 / 1e-200 +#eval 1 / 1e-400 diff --git a/tests/lean/decimals.lean.expected.out b/tests/lean/decimals.lean.expected.out index 4d23e3b4a3..a52cc35e72 100644 --- a/tests/lean/decimals.lean.expected.out +++ b/tests/lean/decimals.lean.expected.out @@ -9,3 +9,16 @@ 3.000000 3.000000 3.000000 +10000000000.000000 +99999999999999986860582406952576489172979654066176.000000 +99999999999999986862573406138718939297648940722396769236245052384850852127440896.000000 +9999999999999998216360018871870109548898901740426374747374488505608317520357971321909184780648316928.000000 +99999999999999996973312221251036165947450327545502362648241750950346848435554075534196338404706251868027512415973882408182135734368278484639385041047239877871023591066789981811181813306167128854888448.000000 +999999999999999903803069407426113968898218766118103141789833949572356552411722264192305659040010509526872994217248819197070144216063125530186267630296136203765329090687113225440746189048800695790727969805197112921161540803823920273299782054992133678869364753954248541633605124057805104488924519071744.000000 +inf +10.000000 +100.000000 +10000000000.000000 +10000000000000000159028911097599180468360808563945281389781327557747838772170381060813469985856815104.000000 +99999999999999996973312221251036165947450327545502362648241750950346848435554075534196338404706251868027512415973882408182135734368278484639385041047239877871023591066789981811181813306167128854888448.000000 +inf