core / init.data.char.basic

source

@[reducible]

def is_valid_char (n : ℕ) :

Prop

Equations

is_valid_char n = (n < 55296 ∨ 57343 < n ∧ n < 1114112)

source

theorem is_valid_char_range_1 (n : ℕ) (h : n < 55296) :

is_valid_char n

source

theorem is_valid_char_range_2 (n : ℕ) (h₁ : 57343 < n) (h₂ : n < 1114112) :

is_valid_char n

source

structure char :

Type

val : ℕ
valid : is_valid_char self.val

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

Instances for char

source

@[protected, instance]

def char.has_sizeof :

has_sizeof char

Equations

char.has_sizeof = {sizeof := λ (c : char), c.val}

source

@[protected]

def char.lt (a b : char) :

Prop

Equations

a.lt b = (a.val < b.val)

source

@[protected]

def char.le (a b : char) :

Prop

Equations

a.le b = (a.val ≤ b.val)

source

@[protected, instance]

def char.has_lt :

has_lt char

Equations

char.has_lt = {lt := char.lt}

source

@[protected, instance]

def char.has_le :

has_le char

Equations

char.has_le = {le := char.le}

source

@[protected, instance]

def char.decidable_lt (a b : char) :

decidable (a < b)

Equations

a.decidable_lt b = a.val.decidable_lt b.val

source

@[protected, instance]

def char.decidable_le (a b : char) :

decidable (a ≤ b)

Equations

a.decidable_le b = a.val.decidable_le b.val

source

theorem char.zero_lt_d800 :

0 < 55296

source

def char.of_nat (n : ℕ) :

char

Equations

char.of_nat n = dite (is_valid_char n) (λ (h : is_valid_char n), {val := n, valid := h}) (λ (h : ¬is_valid_char n), '\x00')

source

def char.to_nat (c : char) :

ℕ

Equations

c.to_nat = c.val

source

theorem char.eq_of_veq {c d : char} :

c.val = d.val → c = d

source

theorem char.veq_of_eq {c d : char} :

c = d → c.val = d.val

source

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

c ≠ d

source

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

c.val ≠ d.val

source

@[protected, instance]

def char.decidable_eq :

decidable_eq char

Equations

char.decidable_eq = λ (i j : char), decidable_of_decidable_of_iff (nat.decidable_eq i.val j.val) _

source

@[protected, instance]

def char.inhabited :

inhabited char

Equations

char.inhabited = {default := 'A'}