adaptations for leanprover/lean4#12263

kim-em · kim-em · commit 297eedb3d2e1 · 2026-02-02T00:41:22.000Z
diff --git a/Plausible/Sampleable.lean b/Plausible/Sampleable.lean
@@ -118,8 +118,8 @@ class SampleableExt (α : Sort u) where
   [sample : Arbitrary proxy]
   interp : proxy → α
 
-attribute [instance] SampleableExt.proxyRepr
-attribute [instance] SampleableExt.shrink
+attribute [instance_reducible, instance] SampleableExt.proxyRepr
+attribute [instance_reducible, instance] SampleableExt.shrink
 
 namespace SampleableExt
 
