Documentation Verification Report

Basic

📁 Source: Batteries/Data/DList/Basic.lean

Statistics

Metric	Count
Definitions `append`, `apply`, `cons`, `empty`, `instAppend`, `instEmptyCollection`, `instInhabited`, `join`, `ofList`, `ofThunk`, `push`, `singleton`, `toList`	13
Theorems `invariant`	1
Total	14

Batteries.DList

Definitions

Name	Category	Theorems
`append` 📖	CompOp	—
`apply` 📖	CompOp	1 math math: `invariant`
`cons` 📖	CompOp	1 math math: `toList_cons`
`empty` 📖	CompOp	1 math math: `toList_empty`
`instAppend` 📖	CompOp	1 math math: `toList_append`
`instEmptyCollection` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`join` 📖	CompOp	—
`ofList` 📖	CompOp	3 math math: `ofThunk_coe`, `ofList_toList`, `toList_ofList`
`ofThunk` 📖	CompOp	2 math math: `singleton_eq_ofThunk`, `ofThunk_coe`
`push` 📖	CompOp	1 math math: `toList_push`
`singleton` 📖	CompOp	2 math math: `singleton_eq_ofThunk`, `toList_singleton`
`toList` 📖	CompOp	7 math math: `toList_empty`, `toList_singleton`, `toList_append`, `toList_push`, `ofList_toList`, `toList_ofList`, `toList_cons`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`invariant` 📖	mathematical	—	`apply`	—	—

---

← Back to Index