diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean index 10d2fa7a6ee4..f5a4706ec3c5 100644 --- a/src/Init/Data/Repr.lean +++ b/src/Init/Data/Repr.lean @@ -103,29 +103,16 @@ instance {p : α → Prop} [Repr α] : Repr (Subtype p) where namespace Nat -def digitChar (n : Nat) : Char := - if n = 0 then '0' else - if n = 1 then '1' else - if n = 2 then '2' else - if n = 3 then '3' else - if n = 4 then '4' else - if n = 5 then '5' else - if n = 6 then '6' else - if n = 7 then '7' else - if n = 8 then '8' else - if n = 9 then '9' else - if n = 0xa then 'a' else - if n = 0xb then 'b' else - if n = 0xc then 'c' else - if n = 0xd then 'd' else - if n = 0xe then 'e' else - if n = 0xf then 'f' else - '*' +def digits : Array Char := + -- Array syntax not available yet + Array.mk ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f'] + +def digitChar (n : Nat) : Char := digits.getD n '*' def toDigitsCore (base : Nat) : Nat → Nat → List Char → List Char | 0, _, ds => ds | fuel+1, n, ds => - let d := digitChar <| n % base; + let d := digitChar (n % base) let n' := n / base; if n' = 0 then d::ds else toDigitsCore base fuel n' (d::ds)