`simp` uglifies `ofScientific` pretty printing

girving commented 5 months ago

Prerequisites

[x] Put an X between the brackets on this line if you have done all of the following:
- Check that your issue is not already filed.
- Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Scientific literals like 0.123712 pretty print nicely, but simp only messes up the pretty printing. Here's an example with no imports:

theorem with_number : (0.123712 : Float) < 0.8482312 := by
  -- Goal print as `0.123712 < 0.8482312`
  simp only
  -- Goal prints as `OfScientific.ofScientific 123712 true 6 < OfScientific.ofScientific 8482312 true 7`
  sorry

Context

Zulip discussion

This came up for me because I'm working on tightening some bounds of nonlinear functions, and weird numbers naturally appear.

Steps to Reproduce

See repro above.

Versions

% lean --version
Lean (version 4.5.0-rc1, commit b614ff1d12bc, Release)

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

eric-wieser commented 5 months ago

A slightly simpler reproduction is #simp 0.5, which also outputs OfScientific.ofScientific ...

hrmacbeth commented 5 months ago

Duplicate of https://github.com/leanprover/lean4/issues/2159?

girving commented 5 months ago

Yep, duplicate, apologies for not noticing the previous issue.

leanprover / lean4