.

leanprover · Oct 31, 2024 · 0764e2a · 0764e2a
1 parent a8802a3
commit 0764e2a
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 8 deletions.
diff --git a/src/Lean/SimpLC/README.md b/src/Lean/SimpLC/README.md
@@ -16,8 +16,8 @@ import Lean.SimpLC.Whitelists
 
 #guard_msgs (drop info) in
 simp_lc check in String Char Float USize UInt64 UInt32 UInt16 UInt8 PLift ULift Prod Sum Range
-  Subtype ByteArray FloatArray List Option Array Int Nat Bool Id Monad LawfulMonad
-  LawfulSingleton Std
+  Subtype ByteArray FloatArray List Option Array Int Nat Bool Id
+  Monad LawfulFunctor LawfulApplicative LawfulMonad LawfulSingleton Std
 ```
 (optionally adding `_root_`).
 

diff --git a/src/Lean/SimpLC/Whitelists.lean b/src/Lean/SimpLC/Whitelists.lean
@@ -28,8 +28,8 @@ if they do not intentionally occupy the root namespace.
 -/
 -- #guard_msgs (drop info) in
 -- simp_lc check in String Char Float USize UInt64 UInt32 UInt16 UInt8 PLift ULift Prod Sum Range
---   Subtype ByteArray FloatArray List Option Array Int Nat Bool Id Monad LawfulMonad
---   LawfulSingleton Std
+--   Subtype ByteArray FloatArray List Option Array Int Nat Bool Id
+--   Monad LawfulFunctor LawfulApplicative LawfulMonad LawfulSingleton Std
 
 /-
 Check *everything*.

diff --git a/src/Lean/SimpLC/Whitelists/Monad.lean b/src/Lean/SimpLC/Whitelists/Monad.lean
@@ -1,8 +1,12 @@
 import Lean.SimpLC.Whitelists.Root
 
--- TODO: move this to the library??
-@[simp] theorem Functor.map_pure [Monad m] [LawfulMonad m] {a : α} : (f <$> pure a : m β) = pure (f a) := by
-  simp [pure, map]
+-- TODO: move this to the library?
+/--
+This is just a duplicate of `LawfulApplicative.map_pure`,
+but sometimes applies when that doesn't.
+-/
+@[simp] theorem LawfulMonad.map_pure' [Monad m] [LawfulMonad m] {a : α} :
+    (f <$> pure a : m β) = pure (f a) := by simp
 
 -- I can't work out why this isn't closed by `Functor.map_map`.
 simp_lc whitelist LawfulMonad.bind_pure_comp bind_map_left
@@ -12,4 +16,4 @@ The actual checks happen in `tests/lean/run/simplc.lean`.
 This commented out command remains here for convenience while debugging.
 -/
 -- #guard_msgs (drop info) in
--- simp_lc check in Monad LawfulMonad _root_ ExceptT
+-- simp_lc check in Monad LawfulMonad LawfulApplicative _root_ ExceptT