From 82f70247477eb79c5ec3989f788f1094c1421ded Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sat, 13 Apr 2024 09:54:10 +0200
Subject: [PATCH] Update src/Init/Control/Basic.lean

---
 src/Init/Control/Basic.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean
index 2e3e7519bf2e..0f9deaecbda6 100644
--- a/src/Init/Control/Basic.lean
+++ b/src/Init/Control/Basic.lean
@@ -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.