Lemmas

📁 Source: Batteries/Data/BitVec/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems `getElem_ofFnBE`, `getElem_ofFnLE`, `getElem_ofFnLEAux`, `getLsb'_ofFnBE`, `getLsb'_ofFnLE`, `getLsbD_ofFnBE`, `getLsbD_ofFnLE`, `getLsb_ofFnBE`, `getLsb_ofFnLE`, `getMsb'_ofFnBE`, `getMsb'_ofFnLE`, `getMsbD_ofFnBE`, `getMsbD_ofFnLE`, `getMsb_ofFnBE`, `getMsb_ofFnLE`, `msb_ofFnBE`, `msb_ofFnLE`, `ofNat_pow`, `toFin_ofFnBE`, `toFin_ofFnLE`, `toFin_ofFnLEAux`, `toInt_ofFnBE`, `toInt_ofFnLE`, `toNat_ofFnBE`, `toNat_ofFnLE`, `toNat_ofFnLEAux`, `toNat_pow`	27
Total	27

BitVec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`getElem_ofFnBE` 📖	mathematical	—	`ofFnBE`	—	`getElem_ofFnLE`
`getElem_ofFnLE` 📖	mathematical	—	`ofFnLE`	—	`getElem_ofFnLEAux`
`getElem_ofFnLEAux` 📖	mathematical	—	`ofFnLEAux`	—	—
`getLsb'_ofFnBE` 📖	mathematical	—	`ofFnBE`	—	`getLsb_ofFnBE`
`getLsb'_ofFnLE` 📖	mathematical	—	`ofFnLE`	—	`getLsb_ofFnLE`
`getLsbD_ofFnBE` 📖	mathematical	—	`ofFnBE`	—	—
`getLsbD_ofFnLE` 📖	mathematical	—	`ofFnLE`	—	—
`getLsb_ofFnBE` 📖	mathematical	—	`ofFnBE`	—	`getElem_ofFnBE`
`getLsb_ofFnLE` 📖	mathematical	—	`ofFnLE`	—	`getElem_ofFnLE`
`getMsb'_ofFnBE` 📖	mathematical	—	`ofFnBE`	—	`getMsb_ofFnBE`
`getMsb'_ofFnLE` 📖	mathematical	—	`ofFnLE`	—	`getMsb_ofFnLE`
`getMsbD_ofFnBE` 📖	mathematical	—	`ofFnBE`	—	—
`getMsbD_ofFnLE` 📖	mathematical	—	`ofFnLE`	—	—
`getMsb_ofFnBE` 📖	mathematical	—	`ofFnBE`	—	`getMsb_ofFnLE`
`getMsb_ofFnLE` 📖	mathematical	—	`ofFnLE`	—	—
`msb_ofFnBE` 📖	mathematical	—	`ofFnBE`	—	—
`msb_ofFnLE` 📖	mathematical	—	`ofFnLE`	—	—
`ofNat_pow` 📖	—	—	—	—	`toNat_pow`
`toFin_ofFnBE` 📖	mathematical	—	`ofFnBE` `Fin.ofBits`	—	`toNat_ofFnBE`
`toFin_ofFnLE` 📖	mathematical	—	`ofFnLE` `Fin.ofBits`	—	`toNat_ofFnLE`
`toFin_ofFnLEAux` 📖	mathematical	—	`ofFnLEAux` `Nat.ofBits`	—	`toNat_ofFnLEAux`
`toInt_ofFnBE` 📖	mathematical	—	`ofFnBE` `Int.ofBits`	—	`toInt_ofFnLE`
`toInt_ofFnLE` 📖	mathematical	—	`ofFnLE` `Int.ofBits`	—	`toNat_ofFnLE`
`toNat_ofFnBE` 📖	mathematical	—	`ofFnBE` `Nat.ofBits`	—	`toNat_ofFnLE`
`toNat_ofFnLE` 📖	mathematical	—	`ofFnLE` `Nat.ofBits`	—	`ofFnLE.eq_1` `toNat_ofFnLEAux` `Nat.ofBits_lt_two_pow`
`toNat_ofFnLEAux` 📖	mathematical	—	`ofFnLEAux` `Nat.ofBits`	—	`Nat.ofBits_succ`
`toNat_pow` 📖	—	—	—	—	—

---

← Back to Index