From 79dc26ecf383d916c2b1c5690621a9b93edb2131 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 15 Apr 2026 13:31:46 -0400
Subject: [PATCH] chore: Update Lean to v4.29.0

---
 LSpec/SlimCheck/Sampleable.lean |  6 ++++--
 flake.lock                      | 18 +++++++++---------
 lean-toolchain                  |  2 +-
 3 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/LSpec/SlimCheck/Sampleable.lean b/LSpec/SlimCheck/Sampleable.lean
index a4d5fe2..1a7878b 100644
--- a/LSpec/SlimCheck/Sampleable.lean
+++ b/LSpec/SlimCheck/Sampleable.lean
@@ -91,13 +91,14 @@ class SampleableExt (α : Sort u) where
   sample : Gen proxy
   interp : proxy → α
 
-attribute [instance] SampleableExt.proxyRepr
-attribute [instance] SampleableExt.shrink
+attribute [reducible, instance] SampleableExt.proxyRepr
+attribute [reducible, instance] SampleableExt.shrink
 
 namespace SampleableExt
 
 /-- Use to generate instance whose purpose is to simply generate values
 of a type directly using the `Gen` monad -/
+@[reducible]
 def mkSelfContained [Repr α] [Shrinkable α] (sample : Gen α) : SampleableExt α where
   proxy := α
   proxyRepr := inferInstance
@@ -176,6 +177,7 @@ instance Bool.sampleableExt : SampleableExt Bool :=
 /-- This can be specialized into customized `SampleableExt Char` instances.
 The resulting instance has `1 / length` chances of making an unrestricted choice of characters
 and it otherwise chooses a character from `chars` with uniform probabilities.  -/
+@[reducible]
 def Char.sampleable (length : Nat) (chars : Array Char) : SampleableExt Char :=
   mkSelfContained do
     let x ← choose Nat 0 length
diff --git a/flake.lock b/flake.lock
index e648170..c13bdc8 100644
--- a/flake.lock
+++ b/flake.lock
@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1769996383,
-        "narHash": "sha256-AnYjnFWgS49RlqX7LrC4uA+sCCDBj0Ry/WOJ5XWAsa0=",
+        "lastModified": 1775087534,
+        "narHash": "sha256-91qqW8lhL7TLwgQWijoGBbiD4t7/q75KTi8NxjVmSmA=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "57928607ea566b5db3ad13af0e57e921e6b12381",
+        "rev": "3107b77cd68437b9a76194f0f7f9c55f2329ca5b",
         "type": "github"
       },
       "original": {
@@ -42,11 +42,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1771875971,
-        "narHash": "sha256-D3PN4o8RtyHEjlAtsLa6M9xRjIwtMUk4pIkfsNSMAvQ=",
+        "lastModified": 1775267043,
+        "narHash": "sha256-yUCn4Wc5kLboN9JHom/SJAknn7aoSEDyerqFq3k7g0I=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "faebfa2e0d7093fea3ffaa493b316bf3449c1dbf",
+        "rev": "56e917e2766385d0b096ea8be9c40ae54bfe138a",
         "type": "github"
       },
       "original": {
@@ -73,11 +73,11 @@
     },
     "nixpkgs-lib": {
       "locked": {
-        "lastModified": 1769909678,
-        "narHash": "sha256-cBEymOf4/o3FD5AZnzC3J9hLbiZ+QDT/KDuyHXVJOpM=",
+        "lastModified": 1774748309,
+        "narHash": "sha256-+U7gF3qxzwD5TZuANzZPeJTZRHS29OFQgkQ2kiTJBIQ=",
         "owner": "nix-community",
         "repo": "nixpkgs.lib",
-        "rev": "72716169fe93074c333e8d0173151350670b824c",
+        "rev": "333c4e0545a6da976206c74db8773a1645b5870a",
         "type": "github"
       },
       "original": {
diff --git a/lean-toolchain b/lean-toolchain
index 4c685fa..14791d7 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.28.0
+leanprover/lean4:v4.29.0