inductive StrataDDM.FormatMode : Type

A format mode selects one of a type's textual representations. default is the type's default representation; the others name alternatives (e.g. a decimal's plain or scientific form). Parsed from a declared marker name by FormatMode.ofString.

• default : FormatMode
• noExponent : FormatMode
• scientific : FormatMode

@[implicit_reducible]

instance StrataDDM.instDecidableEqFormatMode : DecidableEq FormatMode

Equations

• StrataDDM.instDecidableEqFormatMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def StrataDDM.instReprFormatMode.repr : FormatMode → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprFormatMode : Repr FormatMode

Equations

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

def StrataDDM.instInhabitedFormatMode.default : FormatMode

Equations

• StrataDDM.instInhabitedFormatMode.default = StrataDDM.FormatMode.default

@[implicit_reducible]

instance StrataDDM.instInhabitedFormatMode : Inhabited FormatMode

Equations

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

def StrataDDM.FormatMode.ofString : String → Except String FormatMode

Parse a declared mode name. The empty string and "default" both denote the default representation; an unrecognized name is an error rather than a silent fallback, so a typo in a dialect's @[<mode>] marker fails loudly.

Equations

• StrataDDM.FormatMode.ofString "" = Except.ok StrataDDM.FormatMode.default
• StrataDDM.FormatMode.ofString "default" = Except.ok StrataDDM.FormatMode.default
• StrataDDM.FormatMode.ofString "noExponent" = Except.ok StrataDDM.FormatMode.noExponent
• StrataDDM.FormatMode.ofString "scientific" = Except.ok StrataDDM.FormatMode.scientific
• StrataDDM.FormatMode.ofString x✝ = Except.error (toString "unknown format mode '" ++ toString x✝ ++ toString "'")

class StrataDDM.StrataRender (α : Type) : Type

Types whose literal rendering can be selected by a FormatMode. render .default x is the type's default representation.

• render : FormatMode → α → String

@[implicit_reducible]

instance StrataDDM.instStrataRenderDecimal : StrataRender Decimal

Equations

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