Start working on Arith.lean

1 files changed, 2 insertions, 2 deletions

diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
index 97ffa214..1ff34516 100644
--- a/backends/lean/Base/Diverge.lean
+++ b/backends/lean/Base/Diverge.lean
@@ -703,12 +703,12 @@ namespace Ex4
   | leaf (x : a)
   | node (tl : List (Tree a))
 
-  def id_body (f : Tree a → Result (Tree a)) (t : Tree a) : Result (Tree a) :=
+  def id_body (k : Tree a → Result (Tree a)) (t : Tree a) : Result (Tree a) :=
     match t with
     | .leaf x => .ret (.leaf x)
     | .node tl =>
       do
-        let tl ← map f tl
+        let tl ← map k tl
         .ret (.node tl)
 
   theorem id_body_is_valid :