Documentation

Batteries.Data.Char

theorem Char.le_antisymm_iff {x : Char} {y : Char} :
x = y x y y x
theorem Char.le_antisymm {x : Char} {y : Char} (h1 : x y) (h2 : y x) :
x = y
@[deprecated Char.utf8Size_pos]
theorem String.csize_pos (c : Char) :
0 < c.utf8Size

Alias of Char.utf8Size_pos.

@[deprecated Char.utf8Size_le_four]
theorem String.csize_le_4 (c : Char) :
c.utf8Size 4

Alias of Char.utf8Size_le_four.