23. Sum over an append
total adds up a list of numbers. Prove that the total of xs ++ ys is the total of xs plus the total of ys.
1def total : List Nat → Nat
2 | [] => 0
3 | x :: xs => x + total xs
4theorem solution (xs ys : List Nat) : total (xs ++ ys) = total xs + total ys := by
givenLoading editor…
Type
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
xs ys:List Nat
⊢total (xs ++ ys) = total xs + total ys
ReadyLn 1, Col 1Lean 4
Draft saved in this browser