From a73be70607a20d2db500834ab83e99b92d92e17c Mon Sep 17 00:00:00 2001 From: Tom Levy Date: Sun, 5 Apr 2026 21:16:49 +1200 Subject: [PATCH] doc: fix typo in doc of Functor.mapConst (#13285) This PR fixes a typo. --- Additional comment: I found the description hard to read (in part because the term "constant function" is not one I encounter frequently enough, and because there is no explicit constant function in the signature). Would you consider changing the first sentence from "Mapping a constant function" to "Replaces the value in a functor with a constant, retaining the functor's structure" (based on Functor.discard)? Also, I would write `(fun _ => a)` rather than `Function.const _ a`. --------- Co-authored-by: Joachim Breitner --- src/Init/Prelude.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index e55fd8785c..06361a426c 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -145,7 +145,7 @@ Examples: The constant function that ignores its argument. If `a : α`, then `Function.const β a : β → α` is the “constant function with value `a`”. For all -arguments `b : β`, `Function.const β a b = a`. +arguments `b : β`, `Function.const β a b = a`. It is often written directly as `fun _ => a`. Examples: * `Function.const Bool 10 true = 10` @@ -3754,7 +3754,7 @@ class Functor (f : Type u → Type v) : Type (max (u+1) v) where /-- Mapping a constant function. - Given `a : α` and `v : f α`, `mapConst a v` is equivalent to `Function.const _ a <$> v`. For some + Given `a : α` and `v : f β`, `mapConst a v` is equivalent to `(fun _ => a) <$> v`. For some functors, this can be implemented more efficiently; for all other functors, the default implementation may be used. -/