Documentation

Init.Data.Char.Lemmas

theorem Char.le_def {a : Char} {b : Char} :
a b a.val b.val
theorem Char.lt_def {a : Char} {b : Char} :
a < b a.val < b.val
theorem Char.lt_iff_val_lt_val {a : Char} {b : Char} :
a < b a.val < b.val
@[simp]
theorem Char.not_le {a : Char} {b : Char} :
¬a b b < a
@[simp]
theorem Char.not_lt {a : Char} {b : Char} :
¬a < b b a
@[simp]
theorem Char.le_refl (a : Char) :
a a
@[simp]
theorem Char.lt_irrefl (a : Char) :
¬a < a
theorem Char.le_trans {a : Char} {b : Char} {c : Char} :
a bb ca c
theorem Char.lt_trans {a : Char} {b : Char} {c : Char} :
a < bb < ca < c
theorem Char.le_total (a : Char) (b : Char) :
a b b a
theorem Char.lt_asymm {a : Char} {b : Char} (h : a < b) :
¬b < a
theorem Char.ne_of_lt {a : Char} {b : Char} (h : a < b) :
a b
theorem Char.utf8Size_eq (c : Char) :
c.utf8Size = 1 c.utf8Size = 2 c.utf8Size = 3 c.utf8Size = 4
@[simp]
theorem Char.ofNat_toNat (c : Char) :
Char.ofNat c.toNat = c
theorem Char.ext_iff {a : Char} {b : Char} :
a = b a.val = b.val
theorem Char.ext {a : Char} {b : Char} :
a.val = b.vala = b
@[reducible, inline, deprecated Char.utf8Size]
abbrev String.csize (c : Char) :
Equations
Instances For