class OfScientific (α : Type u) : Type u

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

• 1.23 is syntax for OfScientific.ofScientific (nat_lit 123) true (nat_lit 2)
• 121e100 is syntax for OfScientific.ofScientific (nat_lit 121) false (nat_lit 100)

Note the use of nat_lit; there is no wrapping OfNat.ofNat in the resulting term.

• ofScientific (mantissa : Nat) (exponentSign : Bool) (decimalExponent : Nat) : α

  Produces a value from the given mantissa, exponent sign, and decimal exponent. For the exponent sign, true indicates a negative exponent.

  Examples:

  • 1.23 is syntax for OfScientific.ofScientific (nat_lit 123) true (nat_lit 2)
  • 121e100 is syntax for OfScientific.ofScientific (nat_lit 121) false (nat_lit 100)

  Note the use of nat_lit; there is no wrapping OfNat.ofNat in the resulting term.