Equations
- c.is_punctuation = (c ∈ [' ', ',', '.', '?', '!', ';', '-', '\''])
@[instance]
Equations
- char.decidable_is_whitespace = id (λ (c : char), id (list.decidable_mem c [' ', '\t', '\n']))
@[instance]
Equations
- char.decidable_is_upper = id (λ (c : char), id and.decidable)
@[instance]
Equations
- char.decidable_is_lower = id (λ (c : char), id and.decidable)
@[instance]
Equations
- char.decidable_is_alpha = id (λ (c : char), id or.decidable)
@[instance]
Equations
- char.decidable_is_digit = id (λ (c : char), id and.decidable)
@[instance]
Equations
- char.decidable_is_alphanum = id (λ (c : char), id or.decidable)
@[instance]
Equations
- char.decidable_is_punctuation = id (λ (c : char), id (list.decidable_mem c [' ', ',', '.', '?', '!', ';', '-', '\'']))