theorem isValidChar_toUInt32_of {n : ℕ} (h : n.isValidChar) : n.toUInt32.isValidChar

def Char.ofCharCode (n : ℕ) : Char

Equations

• Char.ofCharCode n = if h : n.isValidChar then { val := n.toUInt32, valid := ⋯ } else default

@[irreducible]

def Nat.toStr' (xs : List Char) (n : ℕ) : List Char

Equations

• Nat.toStr' xs n = if n = 0 then xs else have d := n % 10; have n' := n / 10; have c := Char.ofCharCode ('0'.toNat + d); Nat.toStr' (c :: xs) n'

@[instance_reducible]

instance instLinearOrderString_projects : LinearOrder String

Equations

• instLinearOrderString_projects = { toLE := String.instLE, toLT := String.instLT, le_refl := instLinearOrderString_projects._proof_1, le_trans := instLinearOrderString_projects._proof_2, lt_iff_le_not_ge := instLinearOrderString_projects._proof_3, le_antisymm := instLinearOrderString_projects._proof_4, min := fun (a b : String) => if a ≤ b then a else b, max := fun (a b : String) => if a ≤ b then b else a, toOrd := String.instOrd, le_total := instLinearOrderString_projects._proof_5, toDecidableLE := inferInstance, toDecidableEq := decidableEqOfDecidableLE, toDecidableLT := decidableLTOfDecidableLE, min_def := instLinearOrderString_projects._proof_6, max_def := instLinearOrderString_projects._proof_7, compare_eq_compareOfLessAndEq := instLinearOrderString_projects._proof_8 }