Skip to content

Commit a8191ec

Browse files
authored
chore: bump toolchain to v4.29.0-rc1 (#65)
* patches for nightly-2025-01-04, and drop Batteries dependency * fix adaptation note * merge main * fixes for leanprover/lean4#7516 * merge lean-pr-testing-7516 * deprecations * toolchain * list deprecations * bump toolchain * adaptations for leanprover/lean4#12263 * merge lean-pr-testing-12263 * chore: bump toolchain to v4.29.0-rc1
1 parent 55c8532 commit a8191ec

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed

Plausible/Sampleable.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -118,8 +118,8 @@ class SampleableExt (α : Sort u) where
118118
[sample : Arbitrary proxy]
119119
interp : proxy → α
120120

121-
attribute [instance] SampleableExt.proxyRepr
122-
attribute [instance] SampleableExt.shrink
121+
attribute [instance_reducible, instance] SampleableExt.proxyRepr
122+
attribute [instance_reducible, instance] SampleableExt.shrink
123123

124124
namespace SampleableExt
125125

lean-toolchain

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.28.0
1+
leanprover/lean4:v4.29.0-rc1

0 commit comments

Comments
 (0)