Structures · Lean core
OfScientific
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.
- Defined in
- Init.Data.OfScientific.Basic
- Shape
- One type argument · adds ofScientific
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances4
- Rat
- Float
- Float32
- Lean.JsonNumber
How is a type an instance?
Loading the hierarchy index…
Assumed by0
No theorem or definition in Mathlib takes this class as a hypothesis.
Ancestors0
No ancestors.