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

perf: restore kernel-reduction friendly Nat.hasNotBit definition (#11657)

Browse source 
This PR improves upon #11652 by keeping the kernel-reduction-optimized
definition.
This commit is contained in:
Joachim Breitner 2025-12-13 18:00:33 +01:00 • committed by GitHub
parent 38c401cf3b
commit 0bfbb71796
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Init/Data/Nat/Bitwise/Basic.lean
View file

@ -144,7 +144,10 @@ Asserts that the `(n+1)`th least significant bit of `m` is not set.
(This definition is used by Lean internally for compact bitmaps.)
-/
@[expose, reducible] protected def hasNotBit (m n : Nat) : Prop :=
1 &&& (m >>> n) ≠ 1
@[expose] protected def hasNotBit (m n : Nat) : Prop :=
Nat.land 1 (Nat.shiftRight m n) ≠ 1
@[grind =]
theorem hasNotBit_eq (m n : Nat) : Nat.hasNotBit m n = (1 &&& (m >>> n) ≠ 1) := rfl
end Nat