Rationals and Floats

Stream: lean4

[cognivore]

I would like to approximate probabilities to Rationals rather than Floats. What's the best way to do it while still preserving the capability of writing Float literals like 1.0, 0.66, etc?

I don't need full type safety, i.e. for stuff to be within [0, 1], but if you know a way to ensure complete type safety, I'd be very grateful for any hints too :bow:

[Henrik Böving]

docs4#OfScientific is the type class that manages this notation.

[cognivore]

I wonder if there's a way to do approximation, but I'll read Rat.lean more carefully, but I didn't see it there.