Monadic

Statistics

Metric	Count
Definitions	0
Theorems `SatisfiesM_anyM`, `SatisfiesM_anyM_iff_exists`, `SatisfiesM_foldlM`, `SatisfiesM_foldrM`, `SatisfiesM_mapFinIdxM`, `SatisfiesM_mapIdxM`, `SatisfiesM_mapM`, `SatisfiesM_mapM'`, `size_mapFinIdxM`, `size_mapIdxM`, `size_mapM`, `size_modifyM`	12
Total	12

Name	Kind	Assumes	Proves	Validates	Depends On
`SatisfiesM_anyM` 📖	—	`SatisfiesM`	—	—	—
`SatisfiesM_anyM_iff_exists` 📖	—	`SatisfiesM`	—	—	`SatisfiesM.imp` `SatisfiesM_anyM` `SatisfiesM.pure`
`SatisfiesM_foldlM` 📖	—	`SatisfiesM`	—	—	—
`SatisfiesM_foldrM` 📖	—	`SatisfiesM`	—	—	`SatisfiesM.pure`
`SatisfiesM_mapFinIdxM` 📖	—	`SatisfiesM`	—	—	—
`SatisfiesM_mapIdxM` 📖	—	`SatisfiesM`	—	—	`SatisfiesM_mapFinIdxM`
`SatisfiesM_mapM` 📖	—	`SatisfiesM`	—	—	`SatisfiesM.imp` `SatisfiesM_foldlM` `SatisfiesM.map`
`SatisfiesM_mapM'` 📖	—	`SatisfiesM`	—	—	`SatisfiesM.imp` `SatisfiesM_mapM`
`size_mapFinIdxM` 📖	mathematical	—	`SatisfiesM`	—	`SatisfiesM.imp` `SatisfiesM_mapFinIdxM` `SatisfiesM.of_true`
`size_mapIdxM` 📖	mathematical	—	`SatisfiesM`	—	`size_mapFinIdxM`
`size_mapM` 📖	mathematical	—	`SatisfiesM`	—	`SatisfiesM.imp` `SatisfiesM_mapM'` `SatisfiesM.trivial`
`size_modifyM` 📖	mathematical	—	`SatisfiesM`	—	`SatisfiesM.pure` `SatisfiesM.bind_pre` `SatisfiesM.of_true`

---