TermColor.Color: colors and terminal color levels

Color describes a color independently of a terminal. Rendering chooses the strongest representation the target terminal can accept: the eight ANSI colors, the xterm 256-color palette, or 24-bit RGB. default means the terminal's configured default color.

The RGB-to-palette conversions use the conventional xterm palette. A terminal may let its user redefine that palette, so RGB fallback is necessarily an approximation unless the caller chooses a stronger target.

inductive TermColor.BasicColor : Type

The eight ANSI color names.

• black : BasicColor

  Black.

• red : BasicColor

  Red.

• green : BasicColor

  Green.

• yellow : BasicColor

  Yellow.

• blue : BasicColor

  Blue.

• magenta : BasicColor

  Magenta.

• cyan : BasicColor

  Cyan.

• white : BasicColor

  White.

@[instance_reducible]

instance TermColor.instBEqBasicColor : BEq BasicColor

Equations

• TermColor.instBEqBasicColor = { beq := TermColor.instBEqBasicColor.beq }

def TermColor.instBEqBasicColor.beq : BasicColor → BasicColor → Bool

Equations

• TermColor.instBEqBasicColor.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance TermColor.instDecidableEqBasicColor : DecidableEq BasicColor

Equations

• TermColor.instDecidableEqBasicColor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def TermColor.instReprBasicColor.repr : BasicColor → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• TermColor.instReprBasicColor.repr TermColor.BasicColor.red prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.BasicColor.red")).group prec✝
• TermColor.instReprBasicColor.repr TermColor.BasicColor.blue prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.BasicColor.blue")).group prec✝
• TermColor.instReprBasicColor.repr TermColor.BasicColor.cyan prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.BasicColor.cyan")).group prec✝

@[instance_reducible]

instance TermColor.instReprBasicColor : Repr BasicColor

Equations

• TermColor.instReprBasicColor = { reprPrec := TermColor.instReprBasicColor.repr }

inductive TermColor.Intensity : Type

The two intensities of the eight ANSI colors.

• normal : Intensity

  Normal intensity.

• bright : Intensity

  Bright intensity.

def TermColor.instBEqIntensity.beq : Intensity → Intensity → Bool

Equations

• TermColor.instBEqIntensity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance TermColor.instBEqIntensity : BEq Intensity

Equations

• TermColor.instBEqIntensity = { beq := TermColor.instBEqIntensity.beq }

@[instance_reducible]

instance TermColor.instDecidableEqIntensity : DecidableEq Intensity

Equations

• TermColor.instDecidableEqIntensity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def TermColor.instReprIntensity.repr : Intensity → Nat → Std.Format

Equations

• TermColor.instReprIntensity.repr TermColor.Intensity.normal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.Intensity.normal")).group prec✝
• TermColor.instReprIntensity.repr TermColor.Intensity.bright prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.Intensity.bright")).group prec✝

@[instance_reducible]

instance TermColor.instReprIntensity : Repr Intensity

Equations

• TermColor.instReprIntensity = { reprPrec := TermColor.instReprIntensity.repr }

inductive TermColor.Color : Type

A color that can be represented by ANSI SGR color parameters.

• default : Color

  The terminal's configured default color.

• ansi : Intensity → BasicColor → Color

  An ANSI basic color at the given intensity.

• indexed : UInt8 → Color

  An xterm 256-color palette index.

• rgb : UInt8 → UInt8 → UInt8 → Color

  An explicit red, green, and blue color.

@[instance_reducible]

instance TermColor.instBEqColor : BEq Color

Equations

• TermColor.instBEqColor = { beq := TermColor.instBEqColor.beq }

def TermColor.instBEqColor.beq : Color → Color → Bool

Equations

• TermColor.instBEqColor.beq TermColor.Color.default TermColor.Color.default = true
• TermColor.instBEqColor.beq (TermColor.Color.ansi a a_1) (TermColor.Color.ansi b b_1) = (a == b && a_1 == b_1)
• TermColor.instBEqColor.beq (TermColor.Color.indexed a) (TermColor.Color.indexed b) = (a == b)
• TermColor.instBEqColor.beq (TermColor.Color.rgb a a_1 a_2) (TermColor.Color.rgb b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• TermColor.instBEqColor.beq x✝¹ x✝ = false

def TermColor.instDecidableEqColor.decEq (x✝ x✝¹ : Color) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• TermColor.instDecidableEqColor.decEq TermColor.Color.default TermColor.Color.default = isTrue ⋯
• TermColor.instDecidableEqColor.decEq TermColor.Color.default (TermColor.Color.ansi a a_1) = isFalse ⋯
• TermColor.instDecidableEqColor.decEq TermColor.Color.default (TermColor.Color.indexed a) = isFalse ⋯
• TermColor.instDecidableEqColor.decEq TermColor.Color.default (TermColor.Color.rgb a a_1 a_2) = isFalse ⋯
• TermColor.instDecidableEqColor.decEq (TermColor.Color.ansi a a_1) TermColor.Color.default = isFalse ⋯
• TermColor.instDecidableEqColor.decEq (TermColor.Color.ansi a a_1) (TermColor.Color.ansi b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• TermColor.instDecidableEqColor.decEq (TermColor.Color.ansi a a_1) (TermColor.Color.indexed a_2) = isFalse ⋯
• TermColor.instDecidableEqColor.decEq (TermColor.Color.ansi a a_1) (TermColor.Color.rgb a_2 a_3 a_4) = isFalse ⋯
• TermColor.instDecidableEqColor.decEq (TermColor.Color.indexed a) TermColor.Color.default = isFalse ⋯
• TermColor.instDecidableEqColor.decEq (TermColor.Color.indexed a) (TermColor.Color.ansi a_1 a_2) = isFalse ⋯
• TermColor.instDecidableEqColor.decEq (TermColor.Color.indexed a) (TermColor.Color.indexed b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TermColor.instDecidableEqColor.decEq (TermColor.Color.indexed a) (TermColor.Color.rgb a_1 a_2 a_3) = isFalse ⋯
• TermColor.instDecidableEqColor.decEq (TermColor.Color.rgb a a_1 a_2) TermColor.Color.default = isFalse ⋯
• TermColor.instDecidableEqColor.decEq (TermColor.Color.rgb a a_1 a_2) (TermColor.Color.ansi a_3 a_4) = isFalse ⋯
• TermColor.instDecidableEqColor.decEq (TermColor.Color.rgb a a_1 a_2) (TermColor.Color.indexed a_3) = isFalse ⋯

@[instance_reducible]

instance TermColor.instDecidableEqColor : DecidableEq Color

Equations

• TermColor.instDecidableEqColor = TermColor.instDecidableEqColor.decEq

@[instance_reducible]

instance TermColor.instReprColor : Repr Color

Equations

• TermColor.instReprColor = { reprPrec := TermColor.instReprColor.repr }

def TermColor.instReprColor.repr : Color → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• TermColor.instReprColor.repr TermColor.Color.default prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.Color.default")).group prec✝

def TermColor.Color.black : Color

The ordinary ANSI colors.

Equations

• TermColor.Color.black = TermColor.Color.ansi TermColor.Intensity.normal TermColor.BasicColor.black

def TermColor.Color.red : Color

The ordinary red ANSI color.

Equations

• TermColor.Color.red = TermColor.Color.ansi TermColor.Intensity.normal TermColor.BasicColor.red

def TermColor.Color.green : Color

The ordinary green ANSI color.

Equations

• TermColor.Color.green = TermColor.Color.ansi TermColor.Intensity.normal TermColor.BasicColor.green

def TermColor.Color.yellow : Color

The ordinary yellow ANSI color.

Equations

• TermColor.Color.yellow = TermColor.Color.ansi TermColor.Intensity.normal TermColor.BasicColor.yellow

def TermColor.Color.blue : Color

The ordinary blue ANSI color.

Equations

• TermColor.Color.blue = TermColor.Color.ansi TermColor.Intensity.normal TermColor.BasicColor.blue

def TermColor.Color.magenta : Color

The ordinary magenta ANSI color.

Equations

• TermColor.Color.magenta = TermColor.Color.ansi TermColor.Intensity.normal TermColor.BasicColor.magenta

def TermColor.Color.cyan : Color

The ordinary cyan ANSI color.

Equations

• TermColor.Color.cyan = TermColor.Color.ansi TermColor.Intensity.normal TermColor.BasicColor.cyan

def TermColor.Color.white : Color

The ordinary white ANSI color.

Equations

• TermColor.Color.white = TermColor.Color.ansi TermColor.Intensity.normal TermColor.BasicColor.white

def TermColor.Color.brightBlack : Color

The bright black ANSI color.

Equations

• TermColor.Color.brightBlack = TermColor.Color.ansi TermColor.Intensity.bright TermColor.BasicColor.black

def TermColor.Color.brightRed : Color

The bright red ANSI color.

Equations

• TermColor.Color.brightRed = TermColor.Color.ansi TermColor.Intensity.bright TermColor.BasicColor.red

def TermColor.Color.brightGreen : Color

The bright green ANSI color.

Equations

• TermColor.Color.brightGreen = TermColor.Color.ansi TermColor.Intensity.bright TermColor.BasicColor.green

def TermColor.Color.brightYellow : Color

The bright yellow ANSI color.

Equations

• TermColor.Color.brightYellow = TermColor.Color.ansi TermColor.Intensity.bright TermColor.BasicColor.yellow

def TermColor.Color.brightBlue : Color

The bright blue ANSI color.

Equations

• TermColor.Color.brightBlue = TermColor.Color.ansi TermColor.Intensity.bright TermColor.BasicColor.blue

def TermColor.Color.brightMagenta : Color

The bright magenta ANSI color.

Equations

• TermColor.Color.brightMagenta = TermColor.Color.ansi TermColor.Intensity.bright TermColor.BasicColor.magenta

def TermColor.Color.brightCyan : Color

The bright cyan ANSI color.

Equations

• TermColor.Color.brightCyan = TermColor.Color.ansi TermColor.Intensity.bright TermColor.BasicColor.cyan

def TermColor.Color.brightWhite : Color

The bright white ANSI color.

Equations

• TermColor.Color.brightWhite = TermColor.Color.ansi TermColor.Intensity.bright TermColor.BasicColor.white

def TermColor.Color.hue (degrees : Nat) : Color

The fully saturated, full-brightness color at a hue given in degrees.

The hue wheel wraps, so any Nat is a valid argument. Saturation and value are fixed at their maximum, which is what gradients and rainbows want; for anything else build .rgb directly.

Equations

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

def TermColor.Color.ansiIndex : Intensity → BasicColor → UInt8

The xterm index of an ANSI color.

Equations

• TermColor.Color.ansiIndex TermColor.Intensity.normal x✝ = UInt8.ofNat (TermColor.Color.basicIndex✝ x✝)
• TermColor.Color.ansiIndex TermColor.Intensity.bright x✝ = UInt8.ofNat (8 + TermColor.Color.basicIndex✝ x✝)

def TermColor.Color.rgbToAnsi256 (r g b : UInt8) : UInt8

The xterm 256-color index nearest to an RGB color.

The 6×6×6 cube is used for chromatic colors and the 8..238 grayscale ramp for exact grays; pure black and white use the exact ANSI-16 endpoints.

Equations

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

def TermColor.Color.ansi256Rgb (index : UInt8) : Nat × Nat × Nat

The conventional RGB value represented by an xterm 256-color index.

Equations

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

def TermColor.Color.rgbToAnsi16 (r g b : UInt8) : UInt8

The ANSI-16 index nearest to an RGB color, using the conventional xterm palette.

Equations

• TermColor.Color.rgbToAnsi16 r g b = TermColor.Color.nearestAnsi16✝ r.toNat g.toNat b.toNat

def TermColor.Color.toAnsi256 : Color → Option UInt8

The xterm 256-color index represented by a color when a palette fallback is needed.

Equations

• TermColor.Color.default.toAnsi256 = none
• (TermColor.Color.ansi a a_1).toAnsi256 = some (TermColor.Color.ansiIndex a a_1)
• (TermColor.Color.indexed a).toAnsi256 = some a
• (TermColor.Color.rgb a a_1 a_2).toAnsi256 = some (TermColor.Color.rgbToAnsi256 a a_1 a_2)

def TermColor.Color.toAnsi16 : Color → Option UInt8

The ANSI-16 index represented by a color when only the basic palette is available.

Equations

• One or more equations did not get rendered due to their size.
• TermColor.Color.default.toAnsi16 = none
• (TermColor.Color.ansi a a_1).toAnsi16 = some (TermColor.Color.ansiIndex a a_1)
• (TermColor.Color.rgb a a_1 a_2).toAnsi16 = some (TermColor.Color.rgbToAnsi16 a a_1 a_2)

Terminal color levels

inductive TermColor.ColorLevel : Type

The color precision a terminal can receive through SGR.

• none : ColorLevel

  Do not emit color codes.

• ansi16 : ColorLevel

  Emit the ANSI-16 palette.

• ansi256 : ColorLevel

  Emit the xterm 256-color palette.

• trueColor : ColorLevel

  Emit 24-bit RGB colors.

@[instance_reducible]

instance TermColor.instBEqColorLevel : BEq ColorLevel

Equations

• TermColor.instBEqColorLevel = { beq := TermColor.instBEqColorLevel.beq }

def TermColor.instBEqColorLevel.beq : ColorLevel → ColorLevel → Bool

Equations

• TermColor.instBEqColorLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance TermColor.instDecidableEqColorLevel : DecidableEq ColorLevel

Equations

• TermColor.instDecidableEqColorLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TermColor.instReprColorLevel : Repr ColorLevel

Equations

• TermColor.instReprColorLevel = { reprPrec := TermColor.instReprColorLevel.repr }

def TermColor.instReprColorLevel.repr : ColorLevel → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• TermColor.instReprColorLevel.repr TermColor.ColorLevel.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.ColorLevel.none")).group prec✝