Documentation Verification Report

TimeM

📁 Source: Cslib/Algorithms/Lean/TimeM.lean

Statistics

Metric	Count
Definitions `TimeM`, `bind`, `instBindOfAdd`, `instFunctor`, `instMonadOfAddZero`, `instPureOfZero`, `instSeqLeftOfAdd`, `instSeqOfAdd`, `instSeqRightOfAdd`, `pure`, `ret`, `tick`, `time`, `«doElem✓[_]_»`, `«doElem✓_»`, `«term⟪_⟫»`	16
Theorems `ext`, `ext_iff`, `instLawfulMonad`, `ret_bind`, `ret_map`, `ret_pure`, `ret_seq`, `ret_seqLeft`, `ret_seqRight`, `ret_tick`, `time_bind`, `time_map`, `time_pure`, `time_seq`, `time_seqLeft`, `time_seqRight`, `time_tick`	17
Total	33

Cslib.Algorithms.Lean

Definitions

Name	Category	Theorems
`TimeM` 📖	CompData	13 math math: `TimeM.time_seqLeft`, `TimeM.instLawfulMonad`, `TimeM.ret_seqRight`, `TimeM.time_seqRight`, `TimeM.ret_pure`, `TimeM.time_pure`, `TimeM.ret_seq`, `TimeM.ret_map`, `TimeM.ret_bind`, `TimeM.time_bind`, `TimeM.time_map`, `TimeM.ret_seqLeft`, `TimeM.time_seq`

Cslib.Algorithms.Lean.TimeM

Definitions

Name	Category	Theorems
`bind` 📖	CompOp	—
`instBindOfAdd` 📖	CompOp	2 math math: `ret_bind`, `time_bind`
`instFunctor` 📖	CompOp	2 math math: `ret_map`, `time_map`
`instMonadOfAddZero` 📖	CompOp	1 math math: `instLawfulMonad`
`instPureOfZero` 📖	CompOp	2 math math: `ret_pure`, `time_pure`
`instSeqLeftOfAdd` 📖	CompOp	2 math math: `time_seqLeft`, `ret_seqLeft`
`instSeqOfAdd` 📖	CompOp	2 math math: `ret_seq`, `time_seq`
`instSeqRightOfAdd` 📖	CompOp	2 math math: `ret_seqRight`, `time_seqRight`
`pure` 📖	CompOp	—
`ret` 📖	CompOp	18 math math: `ret_seqRight`, `ret_pure`, `ret_merge`, `mergeSort_sorted`, `mergeSort_same_length`, `sorted_merge`, `ret_seq`, `merge_ret_length_eq_sum`, `ret_tick`, `ret_map`, `ext_iff`, `ret_bind`, `time_bind`, `mergeSort_perm`, `ret_seqLeft`, `merge_perm`, `min_all_merge`, `mergeSort_correct`
`tick` 📖	CompOp	2 math math: `time_tick`, `ret_tick`
`time` 📖	CompOp	11 math math: `time_seqLeft`, `merge_time`, `time_seqRight`, `time_pure`, `mergeSort_time`, `time_tick`, `ext_iff`, `time_bind`, `time_map`, `mergeSort_time_le`, `time_seq`
`«doElem✓[_]_»` 📖	CompOp	—
`«doElem✓_»` 📖	CompOp	—
`«term⟪_⟫»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`ret` `time`	—	—	—
`ext_iff` 📖	mathematical	—	`ret` `time`	—	`ext`
`instLawfulMonad` 📖	mathematical	—	`Cslib.Algorithms.Lean.TimeM` `instMonadOfAddZero`	—	`ext`
`ret_bind` 📖	mathematical	—	`ret` `Cslib.Algorithms.Lean.TimeM` `instBindOfAdd`	—	—
`ret_map` 📖	mathematical	—	`ret` `Cslib.Algorithms.Lean.TimeM` `instFunctor`	—	—
`ret_pure` 📖	mathematical	—	`ret` `Cslib.Algorithms.Lean.TimeM` `instPureOfZero`	—	—
`ret_seq` 📖	mathematical	—	`ret` `Cslib.Algorithms.Lean.TimeM` `instSeqOfAdd`	—	—
`ret_seqLeft` 📖	mathematical	—	`ret` `Cslib.Algorithms.Lean.TimeM` `instSeqLeftOfAdd`	—	—
`ret_seqRight` 📖	mathematical	—	`ret` `Cslib.Algorithms.Lean.TimeM` `instSeqRightOfAdd`	—	—
`ret_tick` 📖	mathematical	—	`ret` `tick`	—	—
`time_bind` 📖	mathematical	—	`time` `Cslib.Algorithms.Lean.TimeM` `instBindOfAdd` `ret`	—	—
`time_map` 📖	mathematical	—	`time` `Cslib.Algorithms.Lean.TimeM` `instFunctor`	—	—
`time_pure` 📖	mathematical	—	`time` `Cslib.Algorithms.Lean.TimeM` `instPureOfZero`	—	—
`time_seq` 📖	mathematical	—	`time` `Cslib.Algorithms.Lean.TimeM` `instSeqOfAdd`	—	—
`time_seqLeft` 📖	mathematical	—	`time` `Cslib.Algorithms.Lean.TimeM` `instSeqLeftOfAdd`	—	—
`time_seqRight` 📖	mathematical	—	`time` `Cslib.Algorithms.Lean.TimeM` `instSeqRightOfAdd`	—	—
`time_tick` 📖	mathematical	—	`time` `tick`	—	—

---

← Back to Index