In
import Lean
open Lean Elab Command
set_option doc.verso true
/--
{lean}`aa` works and so does {lean}`hello`
-/
def aa : String := "aa"
/--
{lean}`fwdDecl` works and so does {lean}`aa` but not {CURSOR IS HERE}`mispelled`
-/
def fwdDecl := 2
If my cursor is in the {}, I tried hitting ctrl-space to get suggestions on what available roles are, but nothing came up. Is it possible to have completion for that? I find it especially helpful for DSLs since docs can be sparse.

In
If my cursor is in the
{}, I tried hitting ctrl-space to get suggestions on what available roles are, but nothing came up. Is it possible to have completion for that? I find it especially helpful for DSLs since docs can be sparse.