Documentation Verification Report

ByteSlice

📁 Source: Batteries/Data/ByteSlice.lean

Statistics

Metric	Count
Definitions `ByteSubarray`, `foldl`, `foldlM`, `forIn`, `loop`, `get`, `instForInUInt8OfMonad`, `instGetElemNatUInt8LtSize`, `instStreamUInt8`, `isEmpty`, `pop`, `popFront`, `size`, `start`, `stop`, `toByteArray`, `toByteSubarray`, `foldl`, `foldlM`, `forIn`, `loop`, `instCoeByteArray_batteries`, `instForInUInt8OfMonad_batteries`, `instStreamUInt8_batteries`, `isEmpty`, `pop`, `popFront`, `instCoeByteArrayByteSubarray`	28
Theorems `start_le_stop`, `stop_eq_start_add_size`, `stop_le_array_size`, `stop_eq_start_add_size`	4
Total	32

Batteries

Definitions

Name	Category	Theorems
`ByteSubarray` 📖	CompData	—

Batteries.ByteSubarray

Definitions

Name	Category	Theorems
`foldl` 📖	CompOp	—
`foldlM` 📖	CompOp	—
`forIn` 📖	CompOp	—
`get` 📖	CompOp	—
`instForInUInt8OfMonad` 📖	CompOp	—
`instGetElemNatUInt8LtSize` 📖	CompOp	—
`instStreamUInt8` 📖	CompOp	—
`isEmpty` 📖	CompOp	—
`pop` 📖	CompOp	—
`popFront` 📖	CompOp	—
`size` 📖	CompOp	1 math math: `stop_eq_start_add_size`
`start` 📖	CompOp	2 math math: `start_le_stop`, `stop_eq_start_add_size`
`stop` 📖	CompOp	3 math math: `start_le_stop`, `stop_le_array_size`, `stop_eq_start_add_size`
`toByteArray` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`start_le_stop` 📖	mathematical	—	`start` `stop`	—	—
`stop_eq_start_add_size` 📖	mathematical	—	`stop` `start` `size`	—	`size.eq_1` `start_le_stop`
`stop_le_array_size` 📖	mathematical	—	`stop` `array`	—	—

Batteries.ByteSubarray.forIn

Definitions

Name	Category	Theorems
`loop` 📖	CompOp	—

ByteArray

Definitions

Name	Category	Theorems
`toByteSubarray` 📖	CompOp	—

ByteSlice

Definitions

Name	Category	Theorems
`foldl` 📖	CompOp	—
`foldlM` 📖	CompOp	—
`forIn` 📖	CompOp	—
`instCoeByteArray_batteries` 📖	CompOp	—
`instForInUInt8OfMonad_batteries` 📖	CompOp	—
`instStreamUInt8_batteries` 📖	CompOp	—
`isEmpty` 📖	CompOp	—
`pop` 📖	CompOp	—
`popFront` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stop_eq_start_add_size` 📖	—	—	—	—	—

ByteSlice.forIn

Definitions

Name	Category	Theorems
`loop` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`instCoeByteArrayByteSubarray` 📖	CompOp	—

---

← Back to Index