structure StrataDDM.Decimal : Type

• mantissa : Int
• exponent : Int

@[implicit_reducible]

instance StrataDDM.instDecidableEqDecimal : DecidableEq Decimal

Equations

• StrataDDM.instDecidableEqDecimal = StrataDDM.instDecidableEqDecimal.decEq

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

Equations

• StrataDDM.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 ⋯

@[implicit_reducible]

instance StrataDDM.instInhabitedDecimal : Inhabited Decimal

Equations

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

def StrataDDM.instInhabitedDecimal.default : Decimal

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprDecimal : Repr Decimal

Equations

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

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

Equations

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

def StrataDDM.Decimal.zero : Decimal

Equations

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

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance StrataDDM.Decimal.instToString : ToString Decimal

Equations

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

@[implicit_reducible]

instance StrataDDM.Decimal.instToExpr : Lean.ToExpr Decimal

Equations

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