From e252002bd4a8038c5243471a648b4f83157b8384 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 2 Dec 2025 14:47:49 +1100
Subject: [PATCH] fix: add nolint unusedArguments to Config structure

The derived Repr instance has an unused precedence parameter, which
is flagged by the unusedArguments linter. This is standard for derived
Repr instances.
---
 PFR/Tactic/RPowSimp.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/PFR/Tactic/RPowSimp.lean b/PFR/Tactic/RPowSimp.lean
index 16242ecc..392beb13 100644
--- a/PFR/Tactic/RPowSimp.lean
+++ b/PFR/Tactic/RPowSimp.lean
@@ -16,6 +16,7 @@ structure Context where
   simp : Simp.Result → SimpM Simp.Result
 
 /-- Configuration for `ring_nf`. -/
+@[nolint unusedArguments]
 structure Config where
   /-- the reducibility setting to use when comparing atoms for defeq -/
   red := TransparencyMode.reducible