max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/data/nat/bitwise): use lean::nat_land and lean::nat_lor

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-31 21:55:25 -07:00
parent e87c471e7f
commit d2d2c32c81
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/data/nat/bitwise.lean
View file

@ -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