Lemmas

Statistics

Metric	Count
Definitions	0
Theorems `ofList_toList`, `ofThunk_coe`, `singleton_eq_ofThunk`, `toList_append`, `toList_cons`, `toList_empty`, `toList_ofList`, `toList_push`, `toList_singleton`	9
Total	9

Name	Kind	Assumes	Proves	Validates	Depends On
`ofList_toList` 📖	mathematical	—	`ofList` `toList`	—	—
`ofThunk_coe` 📖	mathematical	—	`ofThunk` `ofList`	—	—
`singleton_eq_ofThunk` 📖	mathematical	—	`singleton` `ofThunk`	—	—
`toList_append` 📖	mathematical	—	`toList` `Batteries.DList` `instAppend`	—	`invariant`
`toList_cons` 📖	mathematical	—	`toList` `cons`	—	—
`toList_empty` 📖	mathematical	—	`toList` `empty`	—	—
`toList_ofList` 📖	mathematical	—	`toList` `ofList`	—	—
`toList_push` 📖	mathematical	—	`toList` `push`	—	`invariant`
`toList_singleton` 📖	mathematical	—	`toList` `singleton`	—	—

---