Simplifying float expression?

Stream: lean4

[Siddhartha Gadgil]

By running a frontend, I have obtained a huge expression for a Float(after reducing) involving .ofScientific and a lot of operations. Is there a way to get the float, say as a string representation. If I apply Float.toString I just get the same expression with the function prepended.

Also the same for Nat. Here I have my code that works, but I remember something in Lean core which I cannot find.

[Eric Wieser]

docs#Lean.Meta.evalExpr ?