Colorized library for adding color and style to text output. This library provides functionality to change the foreground and background colors, as well as to apply various text styles.

inductive Colorized.Section : Type

The Section type represents whether the color applies to the foreground or background.

• Foreground : Section
• Background : Section

inductive Colorized.Color : Type

The Color type represents different color options available for text.

• Black : Color
• Red : Color
• Green : Color
• Yellow : Color
• Blue : Color
• Magenta : Color
• Cyan : Color
• White : Color
• Default : Color

@[implicit_reducible]

instance Colorized.instReprColor : Repr Color

Equations

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

inductive Colorized.Style : Type

The Style type represents different text styles that can be applied.

• Normal : Style
• Bold : Style
• Faint : Style
• Italic : Style
• Underline : Style
• SlowBlink : Style
• ColoredNormal : Style
• Reverse : Style

@[implicit_reducible]

instance Colorized.instReprStyle : Repr Style

Equations

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

class Colorized.Colorized (α : Type) : Type

The Colorized class defines an interface for colorizing and styling text. It provides methods for applying color to the foreground or background, and for applying different text styles.

• colorize : Section → Color → α → α
• style : Style → α → α
• bgColor : Color → α → α
• color : Color → α → α

@[inline]

def Colorized.colorizeString (sec : Section) (col : Color) (str : String) : String

Applies a section/color to a string.

Equations

• Colorized.colorizeString Colorized.Section.Foreground col str = toString Colorized.const✝ ++ toString "9" ++ toString (repr col) ++ toString "m" ++ toString str ++ toString Colorized.reset✝
• Colorized.colorizeString Colorized.Section.Background col str = toString Colorized.const✝ ++ toString "4" ++ toString (repr col) ++ toString "m" ++ toString str ++ toString Colorized.reset✝

@[inline]

def Colorized.stylizeString (sty : Style) (str : String) : String

Applies a style to a string.

Equations

• Colorized.stylizeString sty str = toString Colorized.const✝ ++ toString (repr sty) ++ toString "m" ++ toString str ++ toString Colorized.reset✝

@[implicit_reducible]

instance Colorized.instColorizedString : Colorized String

Equations

• Colorized.instColorizedString = { colorize := Colorized.colorizeString, style := Colorized.stylizeString }