Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-01-29 16:57
0988583c
View on Github →
feat: port Data.Num.Bitwise (
#1919
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Data/Num/Basic.lean
Created
Mathlib/Data/Num/Bitwise.lean
added
def
Num.land
added
def
Num.ldiff
added
def
Num.lor
added
def
Num.lxor
added
def
Num.oneBits
added
def
Num.shiftl
added
def
Num.shiftr
added
def
Num.testBit
added
def
NzsNum.bit0
added
def
NzsNum.bit1
added
def
NzsNum.drec'
added
def
NzsNum.head
added
def
NzsNum.not
added
def
NzsNum.sign
added
def
NzsNum.tail
added
inductive
NzsNum
added
def
PosNum.land
added
def
PosNum.ldiff
added
def
PosNum.lor
added
def
PosNum.lxor
added
def
PosNum.oneBits
added
def
PosNum.shiftl
added
def
PosNum.shiftr
added
def
PosNum.testBit
added
def
SNum.bit0
added
def
SNum.bit1
added
def
SNum.bit
added
theorem
SNum.bit_one
added
theorem
SNum.bit_zero
added
def
SNum.bits
added
def
SNum.cAdd
added
def
SNum.czAdd
added
def
SNum.drec'
added
def
SNum.head
added
def
SNum.not
added
def
SNum.pred
added
def
SNum.rec'
added
def
SNum.sign
added
def
SNum.succ
added
def
SNum.tail
added
def
SNum.testBit
added
inductive
SNum