From d0fb48b4e420d1d2b9cf62e158b3afb4e41d5b68 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 20 Feb 2024 10:21:12 +0100 Subject: [PATCH] fix: use builtin code action for "try this" --- src/Lean/Meta/Tactic/TryThis.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/Tactic/TryThis.lean b/src/Lean/Meta/Tactic/TryThis.lean index 80b30cc27c..46d86605c1 100644 --- a/src/Lean/Meta/Tactic/TryThis.lean +++ b/src/Lean/Meta/Tactic/TryThis.lean @@ -106,7 +106,7 @@ structure TryThisInfo : Type where This is a code action provider that looks for `TryThisInfo` nodes and supplies a code action to apply the replacement. -/ -@[code_action_provider] def tryThisProvider : CodeActionProvider := fun params snap => do +@[builtin_code_action_provider] def tryThisProvider : CodeActionProvider := fun params snap => do let doc ← readDoc pure <| snap.infoTree.foldInfo (init := #[]) fun _ctx info result => Id.run do let .ofCustomInfo { stx, value } := info | result