From 6e6e718f6c9094a98f31503b4d2e6997148f2af3 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 7 Sep 2026 16:49:56 +0000 Subject: [PATCH] fix: cslib `+typeChanged` on two instance-based deprecations MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `downstream: update repo cslib` merge (ffe4553) added `@[deprecated _root_.refl]` on `MJoin.refl` and moved the existing `@[deprecated Relation.ReflGen.stdSymm]` on `ReflGen.symmGen_symm` from `Confluence.lean` into `Foundations/Relation/Basic.lean`. Both replacements are `Std.Refl`/`Std.Symm` instances rather than the lemmas they replace, so since lean4#14600 the deprecation linter reports `The updated constant has a different type`. `cslib` builds with `--wfail`, so those warnings fail the build. The type difference is intended in both cases — callers are meant to go through `_root_.refl` / `Std.Symm.symm` — so mark both with `+typeChanged` (syntax from lean4#14570). --- cslib/Cslib/Foundations/Relation/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cslib/Cslib/Foundations/Relation/Basic.lean b/cslib/Cslib/Foundations/Relation/Basic.lean index aafcddac2..5f632dd03 100644 --- a/cslib/Cslib/Foundations/Relation/Basic.lean +++ b/cslib/Cslib/Foundations/Relation/Basic.lean @@ -57,7 +57,7 @@ theorem SymmGen.to_eqvGen (h : SymmGen r a b) : EqvGen r a b := attribute [scoped grind →] ReflGen.to_eqvGen TransGen.to_eqvGen ReflTransGen.to_eqvGen SymmGen.to_eqvGen -@[deprecated _root_.refl (since := "2026-09-07")] +@[deprecated _root_.refl +typeChanged (since := "2026-09-07")] theorem MJoin.refl (a : α) : MJoin r a a := _root_.refl a theorem MJoin.single (h : ReflTransGen r a b) : MJoin r a b := by @@ -69,7 +69,7 @@ theorem reflTransGen_mono_closed (h₁ : r₁ ≤ r₂) (h₂ : r₂ ≤ ReflTra ext a b exact ⟨ReflTransGen.mono h₁ a b, reflTransGen_closed h₂ a b⟩ -@[deprecated Relation.ReflGen.stdSymm (since := "2026-09-03")] +@[deprecated Relation.ReflGen.stdSymm +typeChanged (since := "2026-09-03")] lemma ReflGen.symmGen_symm : ReflGen (SymmGen r) a b → ReflGen (SymmGen r) b a := Std.Symm.symm a b