Documentation

Init.Data.OfScientific

class OfScientific (α : Type u) :

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

Instances

    Computes m * 2^e.

    Equations
    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
      
      Equations
      @[export lean_float_of_nat]
      def Float.ofNat (n : Nat) :
      Equations
      Instances For
        Equations
        Instances For
          instance instOfNatFloat {n : Nat} :
          Equations
          @[inline, reducible]
          abbrev Nat.toFloat (n : Nat) :
          Equations
          Instances For