Skip to content

Commit

Permalink
Renmae
Browse files Browse the repository at this point in the history
  • Loading branch information
nomeata committed Apr 11, 2024
1 parent 76c6249 commit ab8e3ac
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Init/Data/Repr.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit ab8e3ac

Please sign in to comment.