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

fix: add missing borrow annotations

Browse source
This commit is contained in:
Gabriel Ebner 2021-10-26 20:04:23 +02:00 • committed by Leonardo de Moura
parent 61e0eab23f
commit 95b769cd5d
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Init/Data/Nat/Bitwise.lean
View file

@ -27,17 +27,17 @@ partial def bitwise (f : Bool → Bool → Bool) (n m : Nat) : Nat :=
r+r
@[extern "lean_nat_land"]
def land : Nat → Nat → Nat := bitwise and
def land : @& Nat → @& Nat → Nat := bitwise and
@[extern "lean_nat_lor"]
def lor : Nat → Nat → Nat := bitwise or
def lor : @& Nat → @& Nat → Nat := bitwise or
@[extern "lean_nat_lxor"]
def xor : Nat → Nat → Nat := bitwise bne
def xor : @& Nat → @& Nat → Nat := bitwise bne
@[extern "lean_nat_shiftl"]
def shiftLeft : Nat → Nat → Nat
def shiftLeft : @& Nat → @& Nat → Nat
| n, 0 => n
| n, succ m => shiftLeft (2*n) m
@[extern "lean_nat_shiftr"]
def shiftRight : Nat → Nat → Nat
def shiftRight : @& Nat → @& Nat → Nat
| n, 0 => n
| n, succ m => shiftRight n m / 2