From d2d2c32c814cefec8655475b24d885071c95ea18 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 31 May 2019 21:55:25 -0700 Subject: [PATCH] feat(library/init/data/nat/bitwise): use lean::nat_land and lean::nat_lor --- library/init/data/nat/bitwise.lean | 2 ++ 1 file changed, 2 insertions(+) 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