Int

📁 Source: Batteries/Data/Int.lean

Statistics

Metric	Count
Definitions ofBits, testBit	2
Theorems ofBits_zero, testBit_ofBits, testBit_ofBits_ge, testBit_ofBits_lt	4
Total	6

Int

Definitions

Name	Category	Theorems
ofBits 📖	CompOp	6 math math: ofBits_zero, BitVec.toInt_ofFnLE, testBit_ofBits, BitVec.toInt_ofFnBE, testBit_ofBits_lt, testBit_ofBits_ge
testBit 📖	CompOp	3 math math: testBit_ofBits, testBit_ofBits_lt, testBit_ofBits_ge

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofBits_zero 📖	mathematical	—	ofBits	—	—
testBit_ofBits 📖	mathematical	—	testBit ofBits	—	testBit_ofBits_ge testBit_ofBits_lt
testBit_ofBits_ge 📖	mathematical	—	testBit ofBits	—	Nat.ofBits_lt_two_pow Nat.testBit_ofBits_ge
testBit_ofBits_lt 📖	mathematical	—	testBit ofBits	—	Nat.ofBits_lt_two_pow Nat.testBit_ofBits_lt

---

← Back to Index