Skip to content

Commit

Permalink
Update src/Init/Control/Basic.lean
Browse files Browse the repository at this point in the history
  • Loading branch information
nomeata authored Apr 13, 2024
1 parent 01fd9b7 commit 82f7024
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/Init/Control/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,8 @@ Important instances include
* `Option`, where `failure := none` and `<|>` returns the left-most `some`.
* Parser combinators typically provide an `Applicative` instance for error-handling and
backtracking.
Error recovery and state can interact subtly. For example, the implementation of `Alternative` for `OptionT (StateT σ Id)` keeps modifications made to the state while recovering from failure, while `StateT σ (OptionT Id)` discards them.
-/
-- NB: List instance is in mathlib. Once upstreamed, add
-- * `List`, where `failure` is the empty list and `<|>` concatenates.
Expand Down

0 comments on commit 82f7024

Please sign in to comment.