diff --git a/library/init/data/nat/bitwise.lean b/library/init/data/nat/bitwise.lean index 1642aa2299..006dcf100c 100644 --- a/library/init/data/nat/bitwise.lean +++ b/library/init/data/nat/bitwise.lean @@ -18,7 +18,9 @@ else let r := bitwise n' m' in if f b₁ b₂ then bit1 r else bit0 r +@[extern cpp "lean::nat_land"] def land : Nat → Nat → Nat := bitwise and +@[extern cpp "lean::nat_lor"] def lor : Nat → Nat → Nat := bitwise or end Nat