From 0d05eca2e5481c56ec7a79ceecb5e93553102055 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Sat, 31 May 2025 07:58:12 -0700 Subject: [PATCH] fix: add names to type signature of MonadWithReader.withReader --- src/Init/Prelude.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index d7fe4d774f54..617295d39564 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -3724,7 +3724,7 @@ class MonadWithReader (ρ : outParam (Type u)) (m : Type u → Type v) where During the inner action `x`, reading the value returns `f` applied to the original value. After control returns from `x`, the reader monad's value is restored. -/ - withReader {α : Type u} : (ρ → ρ) → m α → m α + withReader {α : Type u} : (f : ρ → ρ) → (x : m α) → m α export MonadWithReader (withReader)