mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
a3cb39eac9
This PR migrates most remaining tests to the new test suite. It also completes the migration of directories like `tests/lean/run`, meaning that PRs trying to add tests to those old directories will now fail.
32 lines
815 B
Lean4
32 lines
815 B
Lean4
import Lean
|
|
|
|
open Lean Server Lsp RequestM
|
|
|
|
@[code_action_provider]
|
|
def helloProvider : CodeActionProvider := fun params _snap => do
|
|
let doc ← readDoc
|
|
let vi := doc.versionedIdentifier
|
|
let edit : TextEdit := {
|
|
range := params.range,
|
|
newText := "hello!!!"
|
|
}
|
|
let ca : CodeAction := {
|
|
title := "hello world",
|
|
kind? := "quickfix",
|
|
edit? := WorkspaceEdit.ofTextEdit vi edit
|
|
}
|
|
let longRunner : CodeAction := {
|
|
title := "a long-running action",
|
|
kind? := "refactor",
|
|
}
|
|
let lazyResult : IO CodeAction := do
|
|
return { longRunner with
|
|
edit? := WorkspaceEdit.ofTextEdit vi { range := params.range, newText := "lazy result"}
|
|
}
|
|
return #[ca, {eager := longRunner, lazy? := lazyResult}]
|
|
|
|
theorem asdf : (x : Nat) → x = x := by
|
|
intro x
|
|
--^ codeAction
|
|
rfl
|