ByteArray

Statistics

Metric	Count
Definitions `instDecidableEq_batteries`, `map`, `mapM`, `mapMUnsafe`, `loop`, `ofFn`	6
Theorems `data_copySlice`, `data_mkEmpty`, `data_ofFn`, `getElem_eq_data_getElem`, `getElem_ofFn`, `get_append_left`, `get_append_right`, `get_extract`, `get_extract_aux`, `get_ofFn`, `get_push_eq`, `get_push_lt`, `get_set_eq`, `get_set_ne`, `ofFn_succ`, `ofFn_zero`, `set_set`, `size_ofFn`, `size_push`, `size_set`, `uset_eq_set`	21
Total	27

Name	Category	Theorems
`instDecidableEq_batteries` 📖	CompOp	—
`map` 📖	CompOp	—
`mapM` 📖	CompOp	—
`mapMUnsafe` 📖	CompOp	—
`ofFn` 📖	CompOp	5 math math: `size_ofFn`, `ofFn_succ`, `get_ofFn`, `data_ofFn`, `ofFn_zero`

Name	Kind	Assumes	Proves	Validates	Depends On
`data_copySlice` 📖	—	—	—	—	—
`data_mkEmpty` 📖	—	—	—	—	—
`data_ofFn` 📖	mathematical	—	`ofFn`	—	`ofFn_zero` `ofFn_succ`
`getElem_eq_data_getElem` 📖	—	—	—	—	—
`getElem_ofFn` 📖	mathematical	`ofFn`	`size_ofFn`	—	`get_ofFn`
`get_append_left` 📖	—	—	—	—	—
`get_append_right` 📖	—	—	—	—	—
`get_extract` 📖	mathematical	—	`get_extract_aux`	—	`get_extract_aux`
`get_extract_aux` 📖	—	—	—	—	—
`get_ofFn` 📖	mathematical	—	`ofFn` `size_ofFn`	—	`size_ofFn` `data_ofFn`
`get_push_eq` 📖	—	—	—	—	—
`get_push_lt` 📖	mathematical	—	`size_push`	—	—
`get_set_eq` 📖	—	—	—	—	—
`get_set_ne` 📖	mathematical	—	`size_set`	—	—
`ofFn_succ` 📖	mathematical	—	`ofFn`	—	—
`ofFn_zero` 📖	mathematical	—	`ofFn`	—	—
`set_set` 📖	—	—	—	—	—
`size_ofFn` 📖	mathematical	—	`ofFn`	—	`data_ofFn`
`size_push` 📖	—	—	—	—	—
`size_set` 📖	—	—	—	—	—
`uset_eq_set` 📖	—	—	—	—	—

Name	Category	Theorems
`loop` 📖	CompOp	—

---