mathlib3 documentation

core / init.data.char.basic

@[reducible]
def is_valid_char (n : ) :
Prop
Equations
theorem is_valid_char_range_1 (n : ) (h : n < 55296) :
theorem is_valid_char_range_2 (n : ) (h₁ : 57343 < n) (h₂ : n < 1114112) :
structure char  :

The char type represents an unicode scalar value. See http://www.unicode.org/glossary/#unicode_scalar_value).

Instances for char
@[protected, instance]
Equations
@[protected]
def char.lt (a b : char) :
Prop
Equations
@[protected]
def char.le (a b : char) :
Prop
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def char.decidable_lt (a b : char) :
decidable (a < b)
Equations
@[protected, instance]
def char.decidable_le (a b : char) :
Equations
theorem char.zero_lt_d800  :
0 < 55296
def char.of_nat (n : ) :
Equations
def char.to_nat (c : char) :
Equations
theorem char.eq_of_veq {c d : char} :
c.val = d.val c = d
theorem char.veq_of_eq {c d : char} :
c = d c.val = d.val
theorem char.ne_of_vne {c d : char} (h : c.val d.val) :
c d
theorem char.vne_of_ne {c d : char} (h : c d) :
c.val d.val
@[protected, instance]
Equations