max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: builtin_command_code_action for #guard_msgs

Browse source
This commit is contained in:
Leonardo de Moura 2024-02-25 10:42:21 -08:00 • committed by Leonardo de Moura
parent bfb981d465
commit bc8511ccbf
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/GuardMsgs.lean
View file

@ -100,7 +100,7 @@ deriving TypeName
open CodeAction Server RequestM in
/-- A code action which will update the doc comment on a `#guard_msgs` invocation. -/
@[command_code_action guardMsgsCmd]
@[builtin_command_code_action guardMsgsCmd]
def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do
let .node _ ts := node | return #[]
let res := ts.findSome? fun