fix: Inhabited Float produced a bogus run-time value (#6136)

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

src/Init/Data/Float.lean

@@ -31,7 +31,7 @@ opaque floatSpec : FloatSpec := {
 structure Float where
   val : floatSpec.float
 
-instance : Inhabited Float := ⟨{ val := floatSpec.val }⟩
+instance : Nonempty Float := ⟨{ val := floatSpec.val }⟩
 
 @[extern "lean_float_add"] opaque Float.add : Float → Float → Float
 @[extern "lean_float_sub"] opaque Float.sub : Float → Float → Float
@@ -136,6 +136,9 @@ instance : ToString Float where
 
 @[extern "lean_uint64_to_float"] opaque UInt64.toFloat (n : UInt64) : Float
 
+instance : Inhabited Float where
+  default := UInt64.toFloat 0
+
 instance : Repr Float where
   reprPrec n prec := if n < UInt64.toFloat 0 then Repr.addAppParen (toString n) prec else toString n
 

tests/compiler/float.lean

@@ -15,6 +15,7 @@ def tst1 : IO Unit := do
   IO.println (Float.ofInt 0)
   IO.println (Float.ofInt 42)
   IO.println (Float.ofInt (-42))
+  IO.println (default : Float)
   IO.println (0 / 0 : Float).toUInt8
   IO.println (0 / 0 : Float).toUInt16
   IO.println (0 / 0 : Float).toUInt32

tests/compiler/float.lean.expected.out

@@ -13,6 +13,7 @@ true
 0.000000
 42.000000
 -42.000000
+0.000000
 0
 0
 0