lean4-htt/tests/lean/interactive/completionOption.lean
2021-11-26 11:42:54 +01:00

21 lines
470 B
Text

set_option fo
--^ textDocument/completion
set_option format
--^ textDocument/completion
set_option format.in
--^ textDocument/completion
set_option trace.p
--^ textDocument/completion
set_option trace.pp
--^ textDocument/completion
set_option trace.pp.ana
--^ textDocument/completion
set_option trace.pp.analyze
--^ textDocument/completion