Converting a native Float into a Rat?

Stream: new members

[Kevin Cheung]

I would like to do something like the following to convert a native Lean 4 Float into a Rat:

def one_third_approx : Float := 0.3333

def one_third_approx_rat : ℚ :=  toRat one_third_approx

where toRat is my wishful thinking. There is a FP.toRat in mathlib4 but I didn't know how to make it work here. Is there a way to achieve such a conversion?

[Ruben Van de Velde]

Note that FP is unrelated to built-in floats

[Ruben Van de Velde]

Loogle "Found 0 definitions mentioning Rat and Float. ", so I doubt it exists

[Kevin Cheung]

I see. So if one wants to create something like this, what would be the best route? Convert native Float to FP.Float first?