positivity with scientific notation

Stream: mathlib4

[Heather Macbeth]

I'm working off !4#1707, @Thomas Murrills' PR enabling norm_num to recognise scientific notation. I had thought positivity outsourced all its checks about numerals to norm_num, so I was surprised that this fails:

import Mathlib.Tactic.Positivity

example : (0.25:ℚ) = 1/4 := by norm_num -- works

example : (0:ℚ) < 1/4 := by positivity -- works

example : (0:ℚ) < 0.25 := by positivity -- fails

Does positivity need some change to handle scientific notation?

Also tagging @David Renshaw for good measure.

[Thomas Murrills]

New to the code, but I think the only time norm_num is called from positivity is in normNumPositivity, and that doesn't handle rationals yet (it fails if it sees an .isRat result). positivity seems to get away with 1 / 4 because it's equipped to handle /

[Thomas Murrills]

I think I can fix it; I'll open a branch/PR

[Thomas Murrills]

Ok, this should now be fixed by !4#2103 ! @Heather Macbeth, let me know if it works when field-tested! :)