Documentation Verification Report

StackTape

📁 Source: Cslib/Foundations/Data/StackTape.lean

Statistics

Metric	Count
Definitions `StackTape`, `cons`, `head`, `instEmptyCollection`, `instInhabited`, `length`, `map_some`, `nil`, `tail`, `toList`	10
Theorems `cons_head_tail`, `cons_none_nil_toList`, `cons_some_toList`, `empty_eq_nil`, `eq_iff`, `head_cons`, `length_cons_le`, `length_cons_none`, `length_cons_some`, `length_map_some`, `length_nil`, `length_tail_le`, `nil_toList`, `tail_cons`, `toList_getLast?_ne_some_none`	15
Total	25

Turing

Definitions

Name	Category	Theorems
`StackTape` 📖	CompData	1 math math: `StackTape.empty_eq_nil`

Turing.StackTape

Definitions

Name	Category	Theorems
`cons` 📖	CompOp	8 math math: `head_cons`, `length_cons_some`, `cons_none_nil_toList`, `length_cons_none`, `tail_cons`, `length_cons_le`, `cons_some_toList`, `cons_head_tail`
`head` 📖	CompOp	3 math math: `head_cons`, `cons_head_tail`, `eq_iff`
`instEmptyCollection` 📖	CompOp	1 math math: `empty_eq_nil`
`instInhabited` 📖	CompOp	—
`length` 📖	CompOp	6 math math: `length_tail_le`, `length_cons_some`, `length_cons_none`, `length_map_some`, `length_cons_le`, `length_nil`
`map_some` 📖	CompOp	1 math math: `length_map_some`
`nil` 📖	CompOp	4 math math: `cons_none_nil_toList`, `empty_eq_nil`, `nil_toList`, `length_nil`
`tail` 📖	CompOp	4 math math: `length_tail_le`, `tail_cons`, `cons_head_tail`, `eq_iff`
`toList` 📖	CompOp	3 math math: `cons_none_nil_toList`, `cons_some_toList`, `nil_toList`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cons_head_tail` 📖	mathematical	—	`cons` `head` `tail`	—	`eq_iff` `head_cons` `tail_cons`
`cons_none_nil_toList` 📖	mathematical	—	`toList` `cons` `nil`	—	—
`cons_some_toList` 📖	mathematical	—	`toList` `cons`	—	—
`empty_eq_nil` 📖	mathematical	—	`Turing.StackTape` `instEmptyCollection` `nil`	—	—
`eq_iff` 📖	mathematical	—	`head` `tail`	—	—
`head_cons` 📖	mathematical	—	`head` `cons`	—	—
`length_cons_le` 📖	mathematical	—	`length` `cons`	—	—
`length_cons_none` 📖	mathematical	—	`length` `cons`	—	—
`length_cons_some` 📖	mathematical	—	`length` `cons`	—	—
`length_map_some` 📖	mathematical	—	`length` `map_some`	—	—
`length_nil` 📖	mathematical	—	`length` `nil`	—	—
`length_tail_le` 📖	mathematical	—	`length` `tail`	—	—
`nil_toList` 📖	mathematical	—	`toList` `nil`	—	—
`tail_cons` 📖	mathematical	—	`tail` `cons`	—	—
`toList_getLast?_ne_some_none` 📖	—	—	—	—	—

---

← Back to Index