Data.ScientificNotation

Definitions

interface ScientificDisplay : Type -> Type

  Interface for displaying numeric types that dynamically switches between
  standard and scientific notation based on magnitude
  If `forceScientific` is `True`, then we render in scientific notation no
  matter what the value is

Parameters: a
Constraints: Num a
Methods:

showSci : a -> String

Implementations:

ScientificDisplay Double

ScientificDisplay Integer

ScientificDisplay Nat

showSci : ScientificDisplay a => a -> String

Totality: total
Visibility: public export

sciUpperM : Double

  Magnitude above which `Double` values switch to scientific notation.

Totality: total
Visibility: public export

sciLowerM : Double

  Magnitude below which `Double` values switch to scientific notation.

Totality: total
Visibility: public export

defaultScientificPrecision : Nat

  Default precision used by numeric primitives with scientific notation
  This is maximum, trailing zeros are removed.

Totality: total
Visibility: public export

sciSymbol : Char

  Symbol used to denote the exponent in scientific notation, i.e. `1.0e+03`

Totality: total
Visibility: public export

needsScientific : Double -> Bool

  True when `d` is non-zero and outside the range

Totality: total
Visibility: public export

formatExp : Integer -> String

  Format an integer exponent as `e+XX` or `e-XX`.
  `formatExp 5 == "e+05"`
  `formatExp -123 == "e-123"`

Totality: total
Visibility: public export

formatDigits : Nat -> Integer -> String

  Format a non-negative integer as a decimal string.
  `prec` controls how many digits appear after the decimal point
  Input is taken to already be multiplied by `10^prec`
  Zero-padding is added on the left when there are not enough digits.
  ```
  formatDigits 5 314159 == "3.14159"
  formatDigits 3 314159 == "314.159"
  formatDigits 2 5      == "0.05"
  formatDigits 0 42     == "42"
  ```

Totality: total
Visibility: public export

showDoublePrecision : Nat -> Double -> String

  Format a Double in standard notation with a fixed number of decimal places.
  Rounds the last decimal to the nearest digit, and possibly pads with zeros,
  if precision is greater than the number of digits after the decimal point.
  ```
  showDoublePrecision 3 3.14159  == "3.142"
  showDoublePrecision 3 3.14100  == "3.141"
  showDoublePrecision 0 3.14159  == "3"
  showDoublePrecision 4 100.0    == "100.0000"
  ```

Totality: total
Visibility: public export

showDoubleScientific : Nat -> Double -> String

  Format a Double in scientific notation with a fixed number of
  decimal places in the mantissa.
  
  ```
  showDoubleScientific 5 3.14159    == "3.14159e+00"
  showDoubleScientific 5 (-0.005)   == "-5.00000e-03"
  showDoubleScientific 5 100.0      == "1.00000e+02"
  showDoubleScientific 5 0.0000001  == "1.00000e-07"
  ```

Totality: total
Visibility: public export

trimTrailingZeros : String -> String

  Remove trailing zeros after the decimal point, keeping at least one.
  Handles scientific notation, i.e.`"1.0000e-07"` becomes `"1.0e-07"`

Totality: total
Visibility: public export