fix: `Inhabited Float` produced a bogus run-time value

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.74k stars 427 forks source link

Closed Kha closed 5 days ago

Kha commented 5 days ago

This PR fixes the run-time evaluation of (default : Float).

leanprover-community-bot commented 5 days ago

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c8b4f6b511725056b5d0a13ba856fe33a4782c35 --onto 4600bb16fcded0356d20ae232e7f8580c56a5955. (2024-11-20 09:52:49)