class OfScientific (α : Type u) :

For decimal and scientific numbers (e.g., 1.23, 3.12e10). Examples:


    Computes m * 2^e.

    Instances For
      opaque Float.ofScientific (m : Nat) (s : Bool) (e : Nat) :
      @[defaultInstance 501]

      The OfScientific Float must have priority higher than mid since the default instance Neg Int has mid priority.

      #check -42.0 -- must be Float
      @[export lean_float_of_nat]
      def Float.ofNat (n : Nat) :
      Instances For
        Instances For
          @[inline, reducible]
          abbrev Nat.toFloat (n : Nat) :
          Instances For