diff --git a/src/Init/Data/Nat/Bitwise.lean b/src/Init/Data/Nat/Bitwise.lean
index 52a89b7a89..bd4613d58d 100644
--- a/src/Init/Data/Nat/Bitwise.lean
+++ b/src/Init/Data/Nat/Bitwise.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -10,16 +11,21 @@ import Init.Coe
 
 namespace Nat
 
-partial def bitwise (f : Bool → Bool → Bool) : Nat → Nat → Nat | n, m =>
-if n = 0 then      (if f false true then m else 0)
-else if m = 0 then (if f true false then n else 0)
-else
-  let n' := n / 2;
-  let m' := m / 2;
-  let b₁ := n % 2 = 1;
-  let b₂ := m % 2 = 1;
-  let r  := bitwise n' m';
-  if f b₁ b₂ then bit1 r else bit0 r
+partial def bitwise (f : Bool → Bool → Bool) (n m : Nat) : Nat :=
+  if n = 0 then
+    if f false true then m else 0
+  else if m = 0 then
+    if f true false then n else 0
+  else
+    let n' := n / 2
+    let m' := m / 2
+    let b₁ := n % 2 = 1
+    let b₂ := m % 2 = 1
+    let r  := bitwise f n' m'
+    if f b₁ b₂ then
+      bit1 r
+    else
+      bit0 r
 
 @[extern "lean_nat_land"]
 def land : Nat → Nat → Nat := bitwise and