intellij-arend icon indicating copy to clipboard operation
intellij-arend copied to clipboard

Find usages doesn't work for function aliases

Open marat-rkh opened this issue 3 years ago • 0 comments

\func def \alias defalias (n : Nat) : Nat
  | 0 => 0
  | suc n => defalias n
    

\func usage => defalias
  1. Put the caret at defalias at the first line.
  2. Invoke "Find Usages".

Expected: it shows 2 usages. Actual: no usages are shown.

If I do this for def, I will see 2 usages as expected. Also, when I just put the caret at the def both usages are highlighted in the editor. For defalias this doesn't work.

marat-rkh avatar Jan 31 '22 08:01 marat-rkh