max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: Option is a monad again

Browse source 
Maybe it would also be nice to add an explanation (or a link to an explanation) about why `List` is no longer a monad.
This commit is contained in:
Patrick Massot 2022-10-18 23:02:43 +02:00 • committed by Leonardo de Moura
parent 9fd433785b
commit e80cb2eb51
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
doc/lean3changes.md
View file

@ -340,8 +340,7 @@ partial def f (x : Nat) : IO Unit := do
These are changes to the library which may trip up Lean 3 users:
- `Option` and `List` are no longer monads. Instead there is `OptionM`. This was done to avoid some performance traps. For example `o₁ <|> o₂` where `o₁ o₂ : Option α` will evaluate both `o₁` and `o₂` even if `o₁` evaluates to `some x`. This can be a problem if `o₂` requires a lot of compute to evaluate. A zulip discussion on this design choice is [here](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Option.20do.20notation.20regression.3F).
- `List` is no longer a monad.
## Style changes