@[instance]
@[instance]
Equations
- a.decidable_lt b = a.val.decidable_lt b.val
@[instance]
Equations
- a.decidable_le b = a.val.decidable_le b.val
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')
@[instance]
Equations
- char.decidable_eq = λ (i j : char), decidable_of_decidable_of_iff (nat.decidable_eq i.val j.val) _