core / init.data.char.classes

source

def char.is_whitespace (c : char) :

Prop

Equations

c.is_whitespace = (c ∈ [' ', '\t', '\n'])

Instances for char.is_whitespace

char.decidable_is_whitespace

source

def char.is_upper (c : char) :

Prop

Equations

c.is_upper = (c.val ≥ 65 ∧ c.val ≤ 90)

Instances for char.is_upper

char.decidable_is_upper

source

def char.is_lower (c : char) :

Prop

Equations

c.is_lower = (c.val ≥ 97 ∧ c.val ≤ 122)

Instances for char.is_lower

char.decidable_is_lower

source

def char.is_alpha (c : char) :

Prop

Equations

c.is_alpha = (c.is_upper ∨ c.is_lower)

Instances for char.is_alpha

char.decidable_is_alpha

source

def char.is_digit (c : char) :

Prop

Equations

c.is_digit = (c.val ≥ 48 ∧ c.val ≤ 57)

Instances for char.is_digit

char.decidable_is_digit

source

def char.is_alphanum (c : char) :

Prop

Equations

c.is_alphanum = (c.is_alpha ∨ c.is_digit)

Instances for char.is_alphanum

char.decidable_is_alphanum

source

def char.is_punctuation (c : char) :

Prop

Equations

c.is_punctuation = (c ∈ [' ', ',', '.', '?', '!', ';', '-', '\''])

Instances for char.is_punctuation

char.decidable_is_punctuation

source

def char.to_lower (c : char) :

char

Equations

c.to_lower = let n : ℕ := c.to_nat in ite (n ≥ 65 ∧ n ≤ 90) (char.of_nat (n + 32)) c

source

@[protected, instance]

def char.decidable_is_whitespace :

decidable_pred char.is_whitespace

Equations

char.decidable_is_whitespace = id (λ (c : char), id (list.decidable_mem c [' ', '\t', '\n']))

source

@[protected, instance]

def char.decidable_is_upper :

decidable_pred char.is_upper

Equations

char.decidable_is_upper = id (λ (c : char), id and.decidable)

source

@[protected, instance]

def char.decidable_is_lower :

decidable_pred char.is_lower

Equations

char.decidable_is_lower = id (λ (c : char), id and.decidable)

source

@[protected, instance]

def char.decidable_is_alpha :

decidable_pred char.is_alpha

Equations

char.decidable_is_alpha = id (λ (c : char), id or.decidable)

source

@[protected, instance]

def char.decidable_is_digit :

decidable_pred char.is_digit

Equations

char.decidable_is_digit = id (λ (c : char), id and.decidable)

source

@[protected, instance]

def char.decidable_is_alphanum :

decidable_pred char.is_alphanum

Equations

char.decidable_is_alphanum = id (λ (c : char), id or.decidable)

source

@[protected, instance]

def char.decidable_is_punctuation :

decidable_pred char.is_punctuation

Equations

char.decidable_is_punctuation = id (λ (c : char), id (list.decidable_mem c [' ', ',', '.', '?', '!', ';', '-', '\'']))