44 (#295)

Author: TwoFX

HumanEvalLean/HumanEval44.lean

@@ -1,7 +1,18 @@
 module
 
-def change_base : Unit :=
-  ()
+def changeBase (x : Nat) (base : Nat) : String :=
+  String.ofList (Nat.toDigits base x)
+
+example : changeBase 8 3 = "22" := by native_decide
+example : changeBase 9 3 = "100" := by native_decide
+example : changeBase 234 2 = "11101010" := by native_decide
+example : changeBase 16 2 = "10000" := by native_decide
+example : changeBase 8 2 = "1000" := by native_decide
+example : changeBase 7 2 = "111" := by native_decide
+
+theorem ofDigitChars_changeBase {x : Nat} {base : Nat} (hb' : 1 < base) (hb : base ≤ 10) :
+    Nat.ofDigitChars base (changeBase x base).toList 0 = x := by
+  simp [changeBase, Nat.ofDigitChars_toDigits hb' hb]
 
 /-!
 ## Prompt
@@ -51,4 +62,4 @@ def check(candidate):
         assert candidate(x, x + 1) == str(x)
 
 ```
--/
+-/