20 lines
445 B
Text
20 lines
445 B
Text
import Lean
|
|
|
|
open Lean Server Lsp
|
|
|
|
@[codeActionProvider]
|
|
def helloProvider : CodeActionProvider := fun (params : CodeActionParams) => do
|
|
let uri := params.textDocument.uri
|
|
return RequestTask.pure #[{
|
|
title := "hello world",
|
|
kind? := "quickfix",
|
|
edit? := WorkspaceEdit.ofTextEdit uri {
|
|
range := params.range,
|
|
newText := "hello!!!",
|
|
}
|
|
}]
|
|
|
|
theorem asdf : (x : Nat) → x = x := by
|
|
intro x
|
|
--^ codeAction
|
|
rfl
|