lean4-htt/src/Init/Control
Kim Morrison a75a03c077
feat: relate for loops over List with foldlM (#5913)
There are many more lemmas about `foldlM`, so this may be useful for
reasoning about for loops by transforming them into folds.

The transformation includes accounting for monad effects, but does have
a mild performance difference in that short-circuiting on
`ForInStep.done` is replaced by traversing the rest of the list with a
noop.
2024-11-01 02:41:05 +00:00
..
Lawful chore: cleanup unused variables (#5579) 2024-10-02 01:51:22 +00:00
Basic.lean feat: relate for loops over List with foldlM (#5913) 2024-11-01 02:41:05 +00:00
EState.lean chore: snake-case attributes (part 2) 2022-10-19 09:28:08 -07:00
Except.lean chore: fix linter errors (#4502) 2024-06-19 18:24:08 +00:00
ExceptCps.lean chore: reduce usage of refine' (#5042) 2024-08-14 15:14:44 +00:00
Id.lean chore: snake-case attributes (part 2) 2022-10-19 09:28:08 -07:00
Lawful.lean chore: shaking imports in Init.Data.Nat/Int (#3605) 2024-03-05 13:29:35 +00:00
Option.lean chore: fix linter errors (#4502) 2024-06-19 18:24:08 +00:00
Reader.lean chore: fix linter errors (#4502) 2024-06-19 18:24:08 +00:00
State.lean chore: fix linter errors (#4502) 2024-06-19 18:24:08 +00:00
StateCps.lean chore: reduce usage of refine' (#5042) 2024-08-14 15:14:44 +00:00
StateRef.lean chore: cleanup imports (#5825) 2024-10-23 23:51:13 +00:00