def Nat.toDigit (n : Nat) : Char

Equations

• One or more equations did not get rendered due to their size.

def Int.toDigit (n : Int) : Char

Equations

• n.toDigit = n.toNat.toDigit