From 565a70c8e7653f89e264a7d1cd4c73453f218f30 Mon Sep 17 00:00:00 2001 From: Nicolas Rouquette Date: Tue, 24 Feb 2026 08:33:15 -0800 Subject: [PATCH] chore: bump toolchain to v4.29.0-rc2 ReducibilityStatus.instanceReducible was renamed to implicitReducible in Lean 4.29.0-rc2. --- DocGen4/Process/Attributes.lean | 4 ++-- lean-toolchain | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/DocGen4/Process/Attributes.lean b/DocGen4/Process/Attributes.lean index d240d65..b050816 100644 --- a/DocGen4/Process/Attributes.lean +++ b/DocGen4/Process/Attributes.lean @@ -82,7 +82,7 @@ instance : ToString ReducibilityStatus where | .reducible => "reducible" | .semireducible => "semireducible" | .irreducible => "irreducible" - | .instanceReducible => "instance_reducible" + | .implicitReducible => "implicit_reducible" /-- The list of all enum based attributes doc-gen knows about and can recover. @@ -169,7 +169,7 @@ def getReducibility (decl : Name) : MetaM (Option String) := do match status with | .reducible => return some "reducible" | .irreducible => return some "irreducible" - | .instanceReducible => return some "instance_reducible" + | .implicitReducible => return some "implicit_reducible" -- This is the default so we don't print it. | .semireducible => return none diff --git a/lean-toolchain b/lean-toolchain index c7ad81a..283f574 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0-rc1 +leanprover/lean4:v4.29.0-rc2