Snoc

📁 Source: Mathlib/Data/Vector/Snoc.lean

Statistics

Metric	Count
Definitions revCasesOn, revInductionOn, revInductionOn₂, snoc	4
Theorems mapAccumr_nil, mapAccumr_snoc, mapAccumr₂_nil, mapAccumr₂_snoc, map_snoc, map₂_snoc, replicate_succ_to_snoc, reverse_cons, reverse_snoc, snoc_cons, snoc_nil	11
Total	15

List.Vector

Definitions

Name	Category	Theorems
revCasesOn 📖	CompOp	—
revInductionOn 📖	CompOp	—
revInductionOn₂ 📖	CompOp	—
snoc 📖	CompOp	9 math math: mapAccumr_snoc, mapAccumr₂_snoc, map₂_snoc, reverse_cons, replicate_succ_to_snoc, map_snoc, snoc_nil, snoc_cons, reverse_snoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapAccumr_nil 📖	mathematical	—	mapAccumr nil List.Vector	—	—
mapAccumr_snoc 📖	mathematical	—	mapAccumr snoc	—	—
mapAccumr₂_nil 📖	mathematical	—	mapAccumr₂ nil List.Vector	—	—
mapAccumr₂_snoc 📖	mathematical	—	mapAccumr₂ snoc	—	—
map_snoc 📖	mathematical	—	map snoc	—	map_cons
map₂_snoc 📖	mathematical	—	map₂ snoc	—	—
replicate_succ_to_snoc 📖	mathematical	—	replicate snoc	—	replicate_succ snoc_cons
reverse_cons 📖	mathematical	—	reverse cons snoc	—	—
reverse_snoc 📖	mathematical	—	reverse snoc cons	—	—
snoc_cons 📖	mathematical	—	snoc cons	—	—
snoc_nil 📖	mathematical	—	snoc nil cons	—	—

---

← Back to Index