Monadic

📁 Source: Batteries/Data/Vector/Monadic.lean

Statistics

Metric	Count
Definitions	0
Theorems mapFinIdxM_mk, mapIdxM_mk, mapM_mk	3
Total	3

Vector

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapFinIdxM_mk 📖	mathematical	—	MonadSatisfying.satisfying Array.size_mapFinIdxM	—	Array.size_mapFinIdxM MonadSatisfying.val_eq
mapIdxM_mk 📖	mathematical	—	MonadSatisfying.satisfying Array.size_mapIdxM	—	Array.size_mapIdxM MonadSatisfying.val_eq
mapM_mk 📖	mathematical	—	MonadSatisfying.satisfying Array.size_mapM	—	Array.size_mapM MonadSatisfying.val_eq

---

← Back to Index