SplitBy

Statistics

Metric	Count
Definitions	0
Theorems `flatten_splitBy`, `getLast_getLast_splitBy`, `head_head_splitBy`, `isChain_getLast_head_splitBy`, `isChain_of_mem_splitBy`, `ne_nil_of_mem_splitBy`, `nil_notMem_splitBy`, `splitBy_append`, `splitBy_append_cons`, `splitBy_eq_iff`, `splitBy_eq_nil`, `splitBy_flatten`, `splitBy_ne_nil`, `splitBy_nil`, `splitBy_of_isChain`	15
Total	15

Name	Kind	Assumes	Proves	Validates	Depends On
`flatten_splitBy` 📖	—	—	—	—	—
`getLast_getLast_splitBy` 📖	mathematical	—	`splitBy_ne_nil` `ne_nil_of_mem_splitBy`	—	`splitBy_ne_nil` `ne_nil_of_mem_splitBy` `flatten_splitBy` `getLast_getLast_eq_getLast_flatten`
`head_head_splitBy` 📖	mathematical	—	`splitBy_ne_nil` `ne_nil_of_mem_splitBy`	—	`splitBy_ne_nil` `ne_nil_of_mem_splitBy` `flatten_splitBy` `head_head_eq_head_flatten`
`isChain_getLast_head_splitBy` 📖	—	—	—	—	`isChain_nil`
`isChain_of_mem_splitBy` 📖	—	—	—	—	`instIsEmptyFalse`
`ne_nil_of_mem_splitBy` 📖	—	—	—	—	—
`nil_notMem_splitBy` 📖	—	—	—	—	—
`splitBy_append` 📖	—	—	—	—	`eq_or_ne` `splitBy_eq_iff` `flatten_splitBy` `isChain_of_mem_splitBy` `isChain_append` `isChain_getLast_head_splitBy` `ne_nil_of_mem_splitBy` `getLast_getLast_splitBy` `head_head_splitBy`
`splitBy_append_cons` 📖	—	—	—	—	`splitBy_append`
`splitBy_eq_iff` 📖	—	—	—	—	`flatten_splitBy` `nil_notMem_splitBy` `isChain_of_mem_splitBy` `isChain_getLast_head_splitBy` `splitBy_flatten`
`splitBy_eq_nil` 📖	—	—	—	—	`flatten_splitBy`
`splitBy_flatten` 📖	—	—	—	—	`isChain_cons` `head_flatten_eq_head_head` `IsChain.tail`
`splitBy_ne_nil` 📖	—	—	—	—	`Iff.not` `splitBy_eq_nil`
`splitBy_nil` 📖	—	—	—	—	—
`splitBy_of_isChain` 📖	—	—	—	—	`splitBy.eq_2` `instIsEmptyFalse`

---