-
Notifications
You must be signed in to change notification settings - Fork 100
Open
Labels
enhancementNew feature or requestNew feature or request
Description
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 := 2If 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.

Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
enhancementNew feature or requestNew feature or request