From dedf7a8f44fc76dc4bd7360d23af2cd167ea8fe9 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 21 Nov 2025 10:23:14 +0100 Subject: [PATCH] feat: allow setting reducibilityCoreExt in async contexts (#11301) This PR allows setting reducibilityCoreExt in async contexts (e.g. when using `mkSparseCasesOn` in a realizable definition) --- src/Lean/ReducibilityAttrs.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean index 196420fe1f..0bc82b64fc 100644 --- a/src/Lean/ReducibilityAttrs.lean +++ b/src/Lean/ReducibilityAttrs.lean @@ -36,6 +36,12 @@ builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × Reducib statsFn := fun s => "reducibility attribute core extension" ++ Format.line ++ "number of local entries: " ++ format s.size -- attribute is set by `addPreDefinitions` asyncMode := .async .asyncEnv + replay? := some <| fun _oldState newState newItems otherState => + newItems.foldl (init := otherState) fun otherState k => + if let some v := newState.find? k then + otherState.insert k v + else + otherState } builtin_initialize reducibilityExtraExt : SimpleScopedEnvExtension (Name × ReducibilityStatus) (SMap Name ReducibilityStatus) ←