Lean4

13. Digit sum

EasyProgramFree10 points

Write digitSum n, the sum of the decimal digits of n. For example, the digits of 12345 add up to 15.

Dividing by 10 removes the last digit, but n / 10 is not a structural sub-term of n, so Lean has to be convinced that the recursion ends.

Examples

  1. InputdigitSum 12345Output15
  2. InputdigitSum 0Output0
  3. InputdigitSum 9Output9

Submitting also runs 5 hidden tests.

recursionterminationarithmetic

Learn the ideas

Similar problems

Solution.lean
Loading…
Loading editor…
3#guard (digitSum 12345) = (15)
4#guard (digitSum 0) = (0)
5#guard (digitSum 9) = (9)
examples

Run checks your code against the examples and your custom inputs and records nothing. Submit also runs the hidden tests, confirms the axioms your proof uses and records the result. Each uses one compiler check.

ReadyLn 1, Col 1Lean 4
Draft saved in this browser