structure Strata.Decimal : Type

• mantissa : Int
• exponent : Int

def Strata.instDecidableEqDecimal.decEq (x✝ x✝¹ : Decimal) : Decidable (x✝ = x✝¹)

Equations

• Strata.instDecidableEqDecimal.decEq { mantissa := a, exponent := a_1 } { mantissa := b, exponent := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Strata.instDecidableEqDecimal : DecidableEq Decimal

Equations

• Strata.instDecidableEqDecimal = Strata.instDecidableEqDecimal.decEq

instance Strata.instInhabitedDecimal : Inhabited Decimal

Equations

• Strata.instInhabitedDecimal = { default := Strata.instInhabitedDecimal.default }

def Strata.instInhabitedDecimal.default : Decimal

Equations

• Strata.instInhabitedDecimal.default = { mantissa := default, exponent := default }

instance Strata.instReprDecimal : Repr Decimal

Equations

• Strata.instReprDecimal = { reprPrec := Strata.instReprDecimal.repr }

def Strata.instReprDecimal.repr : Decimal → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Strata.Decimal.zero : Decimal

Equations

• Strata.Decimal.zero = { mantissa := 0, exponent := 0 }

def Strata.Decimal.ofInt (x : Int) : Decimal

Equations

• Strata.Decimal.ofInt x = { mantissa := x, exponent := 0 }

def Strata.Decimal.toString (d : Decimal) : String

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Decimal.instToString : ToString Decimal

Equations

• Strata.Decimal.instToString = { toString := Strata.Decimal.instToString._private_1 }

instance Strata.Decimal.instToExpr : Lean.ToExpr Decimal

Equations

• One or more equations did not get rendered due to their size.