From 394f2383d8d0cd9134d4e951b64fb704d266da56 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Sat, 29 Aug 2026 19:58:20 +0000 Subject: [PATCH 1/2] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index b8f3deceb..7fad210be 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-08-27 +leanprover/lean4-pr-releases:pr-release-14968-d1863d1 From c87c3ba1ede6843e8f95951c1be28b29f074f44d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 30 Aug 2026 09:03:31 +0000 Subject: [PATCH 2/2] mathlib4: drop now-unused `Inhabited` binder on `warnAttr` --- mathlib4/Mathlib/Tactic/Translate/Core.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mathlib4/Mathlib/Tactic/Translate/Core.lean b/mathlib4/Mathlib/Tactic/Translate/Core.lean index 98bb65e31..e718491f0 100644 --- a/mathlib4/Mathlib/Tactic/Translate/Core.lean +++ b/mathlib4/Mathlib/Tactic/Translate/Core.lean @@ -902,7 +902,7 @@ def warnAttrCore (stx : Syntax) (f : Environment → Name → Bool) else "" /-- Warn the user when the declaration has a simple scoped attribute. -/ -def warnAttr {α β : Type} [Inhabited β] (stx : Syntax) (attr : SimpleScopedEnvExtension α β) +def warnAttr {α β : Type} (stx : Syntax) (attr : SimpleScopedEnvExtension α β) (f : β → Name → Bool) (thisAttr attrName src tgt : Name) : CoreM Unit := warnAttrCore stx (f <| attr.getState ·) thisAttr attrName src tgt