SplitOn

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

Statistics

Metric	Count
Definitions	0
Theorems intercalate_splitOn, go_acc, go_ne_nil, splitOnP_append_cons, splitOnP_cons, splitOnP_eq_single, splitOnP_first, splitOnP_ne_nil, splitOnP_nil, splitOnP_spec, splitOn_intercalate, splitOn_nil	12
Total	12

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intercalate_splitOn 📖	—	—	—	—	splitOnP_ne_nil splitOnP_cons
splitOnP_append_cons 📖	—	—	—	—	splitOnP_cons splitOnP_ne_nil
splitOnP_cons 📖	—	—	—	—	splitOnP.eq_1 splitOnP.go_acc
splitOnP_eq_single 📖	—	—	—	—	splitOnP_cons forall_mem_of_forall_mem_cons
splitOnP_first 📖	—	—	—	—	splitOnP_append_cons splitOnP_eq_single
splitOnP_ne_nil 📖	—	—	—	—	splitOnP.go_ne_nil
splitOnP_nil 📖	—	—	—	—	—
splitOnP_spec 📖	—	—	—	—	splitOnP_cons splitOnP_ne_nil
splitOn_intercalate 📖	—	—	—	—	splitOnP_eq_single splitOnP_first
splitOn_nil 📖	—	—	—	—	—

List.splitOnP

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
go_acc 📖	—	—	—	—	—
go_ne_nil 📖	—	—	—	—	—

---

← Back to Index