diff --git a/HumanEvalLean/HumanEval44.lean b/HumanEvalLean/HumanEval44.lean index 1dce700..46b8fe2 100644 --- a/HumanEvalLean/HumanEval44.lean +++ b/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) ``` --/ \ No newline at end of file +-/