mathlib documentation

core.init.data.char.basic

def is_valid_char  :
→ Prop

Equations
theorem is_valid_char_range_1 (n : ) :
n < 55296is_valid_char n

theorem is_valid_char_range_2 (n : ) :
57343 < nn < 1114112is_valid_char n

structure char  :
Type

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

@[instance]

Equations
def char.lt  :
charchar → Prop

Equations
def char.le  :
charchar → Prop

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]
def char.decidable_lt (a b : char) :
decidable (a < b)

Equations
@[instance]
def char.decidable_le (a b : char) :

Equations
theorem char.zero_lt_d800  :
0 < 55296

def char.of_nat  :
char

Equations
def char.to_nat  :
char

Equations
theorem char.eq_of_veq {c d : char} :
c.val = d.valc = d

theorem char.veq_of_eq {c d : char} :
c = dc.val = d.val

theorem char.ne_of_vne {c d : char} :
c.val d.valc d

theorem char.vne_of_ne {c d : char} :
c dc.val d.val

@[instance]

Equations