From c1e7c7fa2040729b587e55651b4f0157c4946aeb Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Tue, 18 Aug 2026 22:23:23 +0000 Subject: [PATCH] fix: drop unused section instances on exists_poolPerm_agree (#195) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The theorem is purely finite combinatorics — extending a finite partial injection of the pooled carrier — and uses neither [Countable S.Srt] nor [Countable S.Rel]; a targeted build emitted the unused-section-variable warning. omit both. --- Graphon/RelPooledAcceptance.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Graphon/RelPooledAcceptance.lean b/Graphon/RelPooledAcceptance.lean index bab314e..9495abd 100644 --- a/Graphon/RelPooledAcceptance.lean +++ b/Graphon/RelPooledAcceptance.lean @@ -59,6 +59,7 @@ universe u variable {S : RelSignature.{u}} [Countable S.Srt] [Countable S.Rel] {M : InfiniteRelExchangeableLaw S} {n : ℕ} +omit [Countable S.Srt] [Countable S.Rel] in /-- **Finite agreement by a pooled permutation**: any sortwise embedding into the pooled carrier agrees with a pooled permutation composed with the original embedding, on any finite set of original vertices. The permutation is chosen independently on each sort, which the full mixed