lean4-htt/src/Init/Control
Sebastian Ullrich 8f67db0101 refactor: never implicitly ignore monadic results
Also change `do e; f` to desugar to `e *> f` so that it is affected as well
2020-04-23 11:09:59 -07:00
..
Alternative.lean
Applicative.lean refactor: never implicitly ignore monadic results 2020-04-23 11:09:59 -07:00
Conditional.lean chore: avoid ^do ... 2019-12-11 06:19:12 -08:00
EState.lean refactor: never implicitly ignore monadic results 2020-04-23 11:09:59 -07:00
Except.lean refactor: never implicitly ignore monadic results 2020-04-23 11:09:59 -07:00
Functor.lean refactor: never implicitly ignore monadic results 2020-04-23 11:09:59 -07:00
Id.lean feat: elaborate do notation 2020-01-31 20:11:06 -08:00
Lift.lean feat: extend tryCoeAndLift 2020-02-03 14:30:13 -08:00
Monad.lean refactor: never implicitly ignore monadic results 2020-04-23 11:09:59 -07:00
Option.lean fix: missing [inline] and code idioms that produce low performance code 2020-02-17 19:06:42 -08:00
Reader.lean fix: wrong instance order for several instances 2020-04-08 16:55:48 -07:00
State.lean feat: add StateM.subsingleton 2020-03-02 08:37:55 -08:00