mathlib documentation

core / init.data.char.basic

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  :
Type

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

@[instance]

Equations
def char.lt (a b : char) :
Prop

Equations
def char.le (a b : char) :
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 (n : ) :

Equations
def char.to_nat (c : 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} (h : c.val d.val) :
c d

theorem char.vne_of_ne {c d : char} (h : c d) :
c.val d.val

@[instance]

Equations