diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean index f5a4706ec3c5..2afd2f91f8a1 100644 --- a/src/Init/Data/Repr.lean +++ b/src/Init/Data/Repr.lean @@ -103,11 +103,11 @@ instance {p : α → Prop} [Repr α] : Repr (Subtype p) where namespace Nat -def digits : Array Char := +def digitChars : 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 digitChar (n : Nat) : Char := digitChars.getD n '*' def toDigitsCore (base : Nat) : Nat → Nat → List Char → List Char | 0, _, ds => ds