class Data.FoldCase (α : Type) : Type

Case-folding typeclass. Provides a function to fold a value to a canonical case. $$\text{foldCase} : \alpha \to \alpha$$

• foldCase : α → α

structure Data.CI (α : Type) [FoldCase α] : Type

A case-insensitive wrapper. Stores the original value and a pre-computed case-folded version. Equality and hashing compare only the folded form.

$$\text{CI}(\alpha) = \{ \text{original} : \alpha,\; \text{foldedCase} : \alpha \}$$

Invariant: foldedCase = FoldCase.foldCase original

• original : α

  The original, unmodified value.

• foldedCase : α

  The case-folded value, used for comparison.

• inv : self.foldedCase = FoldCase.foldCase self.original

  Invariant: foldedCase is always the case-folded form of original.

@[inline]

def Data.CI.mk' {α : Type} [FoldCase α] (x : α) : CI α

Smart constructor that computes the folded form automatically. $$\text{mk'}(x) = \text{CI}(x, \text{foldCase}(x))$$

Equations

• Data.CI.mk' x = { original := x, foldedCase := Data.FoldCase.foldCase x, inv := ⋯ }

@[inline]

def Data.CI.map {α β : Type} [FoldCase α] [FoldCase β] (f : α → β) (ci : CI α) : CI β

Map a function over both original and folded values. $$\text{map}(f, \text{CI}(o, fc)) = \text{CI}(f(o), \text{foldCase}(f(o)))$$

Equations

• Data.CI.map f ci = Data.CI.mk' (f ci.original)

@[implicit_reducible]

instance Data.CI.instBEq {α : Type} [FoldCase α] [BEq α] : BEq (CI α)

Equations

• Data.CI.instBEq = { beq := fun (a b : Data.CI α) => a.foldedCase == b.foldedCase }

@[implicit_reducible]

instance Data.CI.instHashable {α : Type} [FoldCase α] [Hashable α] : Hashable (CI α)

Equations

• Data.CI.instHashable = { hash := fun (ci : Data.CI α) => hash ci.foldedCase }

@[implicit_reducible]

instance Data.CI.instOrd {α : Type} [FoldCase α] [Ord α] : Ord (CI α)

Equations

• Data.CI.instOrd = { compare := fun (a b : Data.CI α) => compare a.foldedCase b.foldedCase }

@[implicit_reducible]

instance Data.CI.instToString {α : Type} [FoldCase α] [ToString α] : ToString (CI α)

Equations

• Data.CI.instToString = { toString := fun (ci : Data.CI α) => toString ci.original }

@[implicit_reducible]

instance Data.CI.instRepr {α : Type} [FoldCase α] [Repr α] : Repr (CI α)

Equations

• Data.CI.instRepr = { reprPrec := fun (ci : Data.CI α) (n : Nat) => reprPrec ci.original n }

@[implicit_reducible]

instance Data.CI.instFoldCaseString : FoldCase String

Equations

• Data.CI.instFoldCaseString = { foldCase := fun (s : String) => s.toLower }

@[implicit_reducible]

instance Data.CI.instFoldCaseChar : FoldCase Char

Equations

• Data.CI.instFoldCaseChar = { foldCase := fun (c : Char) => c.toLower }

theorem Data.CI.ci_eq_iff {α : Type} [FoldCase α] [BEq α] (a b : CI α) : (a == b) = (a.foldedCase == b.foldedCase)

Two CI values are equal iff their folded cases are equal.