Gutter icons for recursive calls + graphical tools for debugging termination problems

[sxhya]

Simple recursive calls of a definition/theorem should be marked with a "recursive call" icon:

More complicated recursive calls (case of mutual recursion) should be marked with a special "mutual recursion" icon (which is nonexistent but should be drawn by a graphics designer). It should look like something like this:

When hovering over a recursive call icon the following information should appear:

• link to a documentation page about termination checking in Arend (TBD)

• a baloon should appear in which the FOETUS CallMatrix of a call should be displayed in a graphical form: a small matrix whose cells have colors ('<' sign should correspond to a green cell, a "=" sign should correspond to a yellow cell, ? should correspond to no coloring). It makes sense to draw only nontrivial entries of the matrix (omit rows/columns consisting solely of '?' sign). Matrices should have row/column labels corresponding to parameters/arguments of the call.

• If there is a complicated mutual recursion Show recursion diagram link should be provided in the baloon. Clicking that link should open the Springy diagram graphically depicting whole RecursiveBehavior class as a graph. Vertices of this graph are functions and arrows correspond to calls (call matrices or their composites).

[ice1000]

Can we have the JetBrains UI Designer to make an icon like this? I really want to see one

[ice1000]

JetBrains UI Designer

By that I mean the employees, not the plugin

[sxhya]

Can we have the JetBrains UI Designer to make an icon like this? I really want to see one

Yes, of course