structure StrataDDM.Decimal : Type

• mantissa : Int
• exponent : Int

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.instDecidableEqDecimal : DecidableEq Decimal

Equations

• StrataDDM.instDecidableEqDecimal = StrataDDM.instDecidableEqDecimal.decEq

@[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.

@[implicit_reducible]

instance StrataDDM.instHashableDecimal : Hashable Decimal

Equations

• StrataDDM.instHashableDecimal = { hash := StrataDDM.instHashableDecimal.hash }

def StrataDDM.instHashableDecimal.hash : Decimal → UInt64

Equations

• StrataDDM.instHashableDecimal.hash { mantissa := a, exponent := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

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.toPlainString (d : Decimal) : String

Always expand to a plain decimal literal, with no scientific notation. SMT-LIB has no scientific-notation numeric literal (a form like 142e10 parses as the free symbol e10 applied to a number), so consumers that emit SMT select this via the noExponent format mode.

Equations

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

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

The default rendering: a plain literal within the pretty-print exponent window [-5, 5], and compact scientific notation outside it.

Equations

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

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

Always render in scientific form: raw mantissaeexponent.

Equations

• d.toSciString = toString d.mantissa ++ toString "e" ++ toString d.exponent

@[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.