Documentation Verification Report

Induction

📁 Source: Mathlib/Data/List/Induction.lean

Statistics

Metric	Count
Definitions `bidirectionalRec`, `bidirectionalRecOn`, `recNeNil`, `recOnNeNil`, `reverseRec`, `reverseRecOn`, `twoStepInduction`	7
Theorems `bidirectionalRec_cons_append`, `bidirectionalRec_nil`, `bidirectionalRec_singleton`, `recNeNil_cons`, `recNeNil_singleton`, `reverseRecOn_concat`, `reverseRecOn_nil`, `reverseRec_concat`, `reverseRec_nil`, `twoStepInduction_cons_cons`, `twoStepInduction_nil`, `twoStepInduction_singleton`	12
Total	19

List

Definitions

Name	Category	Theorems
`bidirectionalRec` 📖	CompOp	3 math math: `bidirectionalRec_singleton`, `bidirectionalRec_nil`, `bidirectionalRec_cons_append`
`bidirectionalRecOn` 📖	CompOp	—
`recNeNil` 📖	CompOp	2 math math: `recNeNil_singleton`, `recNeNil_cons`
`recOnNeNil` 📖	CompOp	—
`reverseRec` 📖	CompOp	2 math math: `reverseRec_nil`, `reverseRec_concat`
`reverseRecOn` 📖	CompOp	2 math math: `reverseRecOn_nil`, `reverseRecOn_concat`
`twoStepInduction` 📖	CompOp	3 math math: `twoStepInduction_cons_cons`, `twoStepInduction_singleton`, `twoStepInduction_nil`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bidirectionalRec_cons_append` 📖	mathematical	—	`bidirectionalRec`	—	—
`bidirectionalRec_nil` 📖	mathematical	—	`bidirectionalRec`	—	—
`bidirectionalRec_singleton` 📖	mathematical	—	`bidirectionalRec`	—	—
`recNeNil_cons` 📖	mathematical	—	`recNeNil`	—	—
`recNeNil_singleton` 📖	mathematical	—	`recNeNil`	—	—
`reverseRecOn_concat` 📖	mathematical	—	`reverseRecOn`	—	`reverseRec_concat`
`reverseRecOn_nil` 📖	mathematical	—	`reverseRecOn`	—	`reverseRec_nil`
`reverseRec_concat` 📖	mathematical	—	`reverseRec`	—	—
`reverseRec_nil` 📖	mathematical	—	`reverseRec`	—	—
`twoStepInduction_cons_cons` 📖	mathematical	—	`twoStepInduction`	—	`twoStepInduction.eq_3`
`twoStepInduction_nil` 📖	mathematical	—	`twoStepInduction`	—	`twoStepInduction.eq_1`
`twoStepInduction_singleton` 📖	mathematical	—	`twoStepInduction`	—	`twoStepInduction.eq_2`

---

← Back to Index