From 95b769cd5dbf6e4fe0b76e2e7022ee576cfcb3f9 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 26 Oct 2021 20:04:23 +0200 Subject: [PATCH] fix: add missing borrow annotations --- src/Init/Data/Nat/Bitwise.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Init/Data/Nat/Bitwise.lean b/src/Init/Data/Nat/Bitwise.lean index 4d014d5c09..d8dc69aaf1 100644 --- a/src/Init/Data/Nat/Bitwise.lean +++ b/src/Init/Data/Nat/Bitwise.lean @@ -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