intellij-arend
intellij-arend copied to clipboard
Find usages doesn't work for function aliases
\func def \alias defalias (n : Nat) : Nat
| 0 => 0
| suc n => defalias n
\func usage => defalias
- Put the caret at
defalias
at the first line. - 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.