From 11473f0672698322405d29375cc0e57744fb272e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 7 Sep 2026 14:56:39 +0000 Subject: [PATCH] fix: cslib `+typeChanged` on the `ReflGen.symmGen_symm` deprecation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `downstream: update repo cslib` merge rewrote `Cslib/Foundations/Relation/Confluence.lean` and deprecated `Relation.ReflGen.symmGen_symm` in favour of the `Std.Symm (ReflGen r)` instance `Relation.ReflGen.stdSymm`. Since `lean4#14600` the deprecation linter compares the two types, and an instance is not the lemma it replaces, so it warns; `cslib` builds with `--wfail`, so that is a build failure. The type difference is intended — mark it with `+typeChanged` (syntax from `lean4#14570`). --- cslib/Cslib/Foundations/Relation/Confluence.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cslib/Cslib/Foundations/Relation/Confluence.lean b/cslib/Cslib/Foundations/Relation/Confluence.lean index c00031d2f..68a03e6f9 100644 --- a/cslib/Cslib/Foundations/Relation/Confluence.lean +++ b/cslib/Cslib/Foundations/Relation/Confluence.lean @@ -417,7 +417,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