From ebec1b3a16dfacaf65b8d712693025eb97bc0c53 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Thu, 29 Jan 2026 15:40:43 +1100 Subject: [PATCH] fix: typo in ExtractLetsConfig doc comment (#12174) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR fixes a typo in `ExtractLetsConfig.merge` doc comment. Reported on Zulip: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Typo.20in.20Init.2FMetaTypes.2Elean/near/568698828 🤖 Prepared with Claude Code Co-authored-by: Claude --- src/Init/MetaTypes.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean index 130919dc96..fcbf622800 100644 --- a/src/Init/MetaTypes.lean +++ b/src/Init/MetaTypes.lean @@ -374,7 +374,7 @@ structure ExtractLetsConfig where /-- If true (default: false), eliminate unused lets rather than extract them. -/ usedOnly : Bool := false /-- If true (default: true), reuse local declarations that have syntactically equal values. - Note that even when false, the caching strategy for `extract_let`s may result in fewer extracted let bindings than expected. -/ + Note that even when false, the caching strategy for `extract_lets` may result in fewer extracted let bindings than expected. -/ merge : Bool := true /-- When merging is enabled, if true (default: true), make use of pre-existing local definitions in the local context. -/ useContext : Bool := true