Legacy

📁 Source: Batteries/Data/String/Legacy.lean

Statistics

Metric	Count
Definitions `all`, `any`, `anyAux`, `back`, `contains`, `drop`, `dropWhile`, `find`, `findAux`, `foldl`, `foldlAux`, `foldr`, `foldrAux`, `front`, `map`, `mapAux`, `posOf`, `posOfAux`, `revFind`, `revFindAux`, `revPosOf`, `revPosOfAux`, `take`, `takeWhile`, `all`, `any`, `contains`, `foldl`, `foldr`	29
Theorems	0
Total	29

String.Legacy

Definitions

Name	Category	Theorems
`all` 📖	CompOp	1 math, 1 bridge math: `String.all_eq` bridge: `String.all_iff`
`any` 📖	CompOp	1 math, 1 bridge math: `String.any_eq` bridge: `String.any_iff`
`anyAux` 📖	CompOp	1 math math: `String.anyAux_of_valid`
`back` 📖	CompOp	2 math math: `String.back_eq`, `String.back_eq_get_prev_rawEndPos`
`contains` 📖	CompOp	1 bridge bridge: `String.contains_iff`
`drop` 📖	CompOp	3 math math: `String.drop_eq`, `String.drop_empty`, `String.toList_drop`
`dropWhile` 📖	CompOp	2 math math: `String.dropWhile_eq`, `String.toList_dropWhile`
`find` 📖	CompOp	2 math math: `String.find_of_valid`, `String.posOf_eq`
`findAux` 📖	CompOp	2 math math: `String.posOfAux_eq`, `String.findAux_of_valid`
`foldl` 📖	CompOp	1 math math: `String.foldl_eq`
`foldlAux` 📖	CompOp	1 math math: `String.foldlAux_of_valid`
`foldr` 📖	CompOp	1 math math: `String.foldr_eq`
`foldrAux` 📖	CompOp	1 math math: `String.foldrAux_of_valid`
`front` 📖	CompOp	1 math math: `String.front_eq`
`map` 📖	CompOp	4 math math: `String.map_isEmpty_eq_isEmpty`, `String.map_eq_empty_iff`, `length_map`, `String.map_eq`
`mapAux` 📖	CompOp	1 math math: `String.mapAux_of_valid`
`posOf` 📖	CompOp	1 math math: `String.posOf_eq`
`posOfAux` 📖	CompOp	1 math math: `String.posOfAux_eq`
`revFind` 📖	CompOp	2 math math: `String.revFind_of_valid`, `String.revPosOf_eq`
`revFindAux` 📖	CompOp	2 math math: `String.revFindAux_of_valid`, `String.revPosOfAux_eq`
`revPosOf` 📖	CompOp	1 math math: `String.revPosOf_eq`
`revPosOfAux` 📖	CompOp	1 math math: `String.revPosOfAux_eq`
`take` 📖	CompOp	2 math math: `String.take_eq`, `String.toList_take`
`takeWhile` 📖	CompOp	2 math math: `String.toList_takeWhile`, `String.takeWhile_eq`

Substring.Raw.Legacy

Definitions

Name	Category	Theorems
`all` 📖	CompOp	2 math math: `Substring.Raw.ValidFor.all`, `Substring.Raw.Valid.all`
`any` 📖	CompOp	2 math math: `Substring.Raw.Valid.any`, `Substring.Raw.ValidFor.any`
`contains` 📖	CompOp	2 bridge bridge: `Substring.Raw.ValidFor.contains`, `Substring.Raw.Valid.contains`
`foldl` 📖	CompOp	2 math math: `Substring.Raw.ValidFor.foldl`, `Substring.Raw.Valid.foldl`
`foldr` 📖	CompOp	2 math math: `Substring.Raw.ValidFor.foldr`, `Substring.Raw.Valid.foldr`

---

← Back to Index