leanprover/lean4

Call hierarchy and recursion

Opened this issue · 1 comments

The very useful Call Hierarchy feature shows recursive calls. I see how that can make sense, but I wonder if not counting the recursive calls as occurrences here would be better - the kind of infinite unfolding we can do here is maybe a bit silly:

recursion

Versions

0c9f9ab

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

I think this is standard behavior for Call hierarchy. It might be good to double check from other language plugins though. (Just checked, this is the case for rust-analyzer)