Documentation Verification Report

Bitwise

📁 Source: Mathlib/Data/Num/Bitwise.lean

Statistics

Metric	Count
Definitions `instAndOp`, `instHShiftLeftNat`, `instHShiftRightNat`, `instOrOp`, `instXorOp`, `land`, `ldiff`, `lor`, `lxor`, `oneBits`, `shiftl`, `shiftr`, `testBit`, `NzsNum`, `bit0`, `bit1`, `drec'`, `head`, `not`, `sign`, `tail`, `«term_::_»`, `«term~_»`, `instHAndNum`, `instHShiftLeftNat`, `instHShiftRightNatNum`, `instHXorNum`, `instOrOp`, `land`, `ldiff`, `lor`, `lxor`, `oneBits`, `shiftl`, `shiftr`, `testBit`, `SNum`, `add`, `bit`, `bit0`, `bit1`, `bits`, `cAdd`, `czAdd`, `drec'`, `head`, `instAdd`, `instMul`, `instNeg`, `instSub`, `mul`, `neg`, `not`, `pred`, `rec'`, `sign`, `sub`, `succ`, `tail`, `testBit`, `«term_::_»`, `«term~_»`, `instCoeNzsNumSNum`, `instDecidableEqNzsNum`, `decEq`, `instDecidableEqSNum`, `decEq`, `instInhabitedNzsNum`, `instInhabitedSNum`, `instOneNzsNum`, `instOneSNum`, `instZeroSNum`	72
Theorems `land_eq_and`, `lor_eq_or`, `lxor_eq_xor`, `shiftl_eq_shiftLeft`, `shiftr_eq_shiftRight`, `land_eq_and`, `lor_eq_or`, `lxor_eq_xor`, `shiftl_eq_shiftLeft`, `shiftl_succ_eq_bit0_shiftl`, `shiftr_eq_shiftRight`, `bit_one`, `bit_zero`	13
Total	85

Num

Definitions

Name	Category	Theorems
`instAndOp` 📖	CompOp	2 math math: `castNum_and`, `land_eq_and`
`instHShiftLeftNat` 📖	CompOp	2 math math: `castNum_shiftLeft`, `shiftl_eq_shiftLeft`
`instHShiftRightNat` 📖	CompOp	2 math math: `castNum_shiftRight`, `shiftr_eq_shiftRight`
`instOrOp` 📖	CompOp	2 math math: `castNum_or`, `lor_eq_or`
`instXorOp` 📖	CompOp	2 math math: `castNum_xor`, `lxor_eq_xor`
`land` 📖	CompOp	1 math math: `land_eq_and`
`ldiff` 📖	CompOp	1 math math: `castNum_ldiff`
`lor` 📖	CompOp	1 math math: `lor_eq_or`
`lxor` 📖	CompOp	1 math math: `lxor_eq_xor`
`oneBits` 📖	CompOp	—
`shiftl` 📖	CompOp	1 math math: `shiftl_eq_shiftLeft`
`shiftr` 📖	CompOp	1 math math: `shiftr_eq_shiftRight`
`testBit` 📖	CompOp	1 math math: `castNum_testBit`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`land_eq_and` 📖	mathematical	—	`land` `Num` `instAndOp`	—	—
`lor_eq_or` 📖	mathematical	—	`lor` `Num` `instOrOp`	—	—
`lxor_eq_xor` 📖	mathematical	—	`lxor` `Num` `instXorOp`	—	—
`shiftl_eq_shiftLeft` 📖	mathematical	—	`shiftl` `Num` `instHShiftLeftNat`	—	—
`shiftr_eq_shiftRight` 📖	mathematical	—	`shiftr` `Num` `instHShiftRightNat`	—	—

NzsNum

Definitions

Name	Category	Theorems
`bit0` 📖	CompOp	—
`bit1` 📖	CompOp	—
`drec'` 📖	CompOp	—
`head` 📖	CompOp	—
`not` 📖	CompOp	—
`sign` 📖	CompOp	—
`tail` 📖	CompOp	—
`«term_::_»` 📖	CompOp	—
`«term~_»` 📖	CompOp	—

PosNum

Definitions

Name	Category	Theorems
`instHAndNum` 📖	CompOp	1 math math: `land_eq_and`
`instHShiftLeftNat` 📖	CompOp	2 math math: `shiftl_eq_shiftLeft`, `shiftl_succ_eq_bit0_shiftl`
`instHShiftRightNatNum` 📖	CompOp	1 math math: `shiftr_eq_shiftRight`
`instHXorNum` 📖	CompOp	1 math math: `lxor_eq_xor`
`instOrOp` 📖	CompOp	1 math math: `lor_eq_or`
`land` 📖	CompOp	1 math math: `land_eq_and`
`ldiff` 📖	CompOp	—
`lor` 📖	CompOp	1 math math: `lor_eq_or`
`lxor` 📖	CompOp	1 math math: `lxor_eq_xor`
`oneBits` 📖	CompOp	—
`shiftl` 📖	CompOp	1 math math: `shiftl_eq_shiftLeft`
`shiftr` 📖	CompOp	1 math math: `shiftr_eq_shiftRight`
`testBit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`land_eq_and` 📖	mathematical	—	`land` `PosNum` `Num` `instHAndNum`	—	—
`lor_eq_or` 📖	mathematical	—	`lor` `PosNum` `instOrOp`	—	—
`lxor_eq_xor` 📖	mathematical	—	`lxor` `PosNum` `Num` `instHXorNum`	—	—
`shiftl_eq_shiftLeft` 📖	mathematical	—	`shiftl` `PosNum` `instHShiftLeftNat`	—	—
`shiftl_succ_eq_bit0_shiftl` 📖	mathematical	—	`PosNum` `instHShiftLeftNat` `bit0`	—	—
`shiftr_eq_shiftRight` 📖	mathematical	—	`shiftr` `PosNum` `Num` `instHShiftRightNatNum`	—	—

SNum

Definitions

Name	Category	Theorems
`add` 📖	CompOp	—
`bit` 📖	CompOp	2 math math: `bit_zero`, `bit_one`
`bit0` 📖	CompOp	—
`bit1` 📖	CompOp	—
`bits` 📖	CompOp	—
`cAdd` 📖	CompOp	—
`czAdd` 📖	CompOp	—
`drec'` 📖	CompOp	—
`head` 📖	CompOp	—
`instAdd` 📖	CompOp	—
`instMul` 📖	CompOp	—
`instNeg` 📖	CompOp	—
`instSub` 📖	CompOp	—
`mul` 📖	CompOp	—
`neg` 📖	CompOp	—
`not` 📖	CompOp	—
`pred` 📖	CompOp	—
`rec'` 📖	CompOp	—
`sign` 📖	CompOp	—
`sub` 📖	CompOp	—
`succ` 📖	CompOp	—
`tail` 📖	CompOp	—
`testBit` 📖	CompOp	—
`«term_::_»` 📖	CompOp	—
`«term~_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bit_one` 📖	mathematical	—	`bit` `zero` `nz` `NzsNum.msb`	—	—
`bit_zero` 📖	mathematical	—	`bit` `zero`	—	—

(root)

Definitions

Name	Category	Theorems
`NzsNum` 📖	CompData	—
`SNum` 📖	CompData	—
`instCoeNzsNumSNum` 📖	CompOp	—
`instDecidableEqNzsNum` 📖	CompOp	—
`instDecidableEqSNum` 📖	CompOp	—
`instInhabitedNzsNum` 📖	CompOp	—
`instInhabitedSNum` 📖	CompOp	—
`instOneNzsNum` 📖	CompOp	—
`instOneSNum` 📖	CompOp	—
`instZeroSNum` 📖	CompOp	—

instDecidableEqNzsNum

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

instDecidableEqSNum

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

---

← Back to Index