Consider showing a type hint for function clauses

[marat-rkh]

Consider the following function:

\func -'+assoc (m n p : Nat): m -' n -' p = m -' (n + p)
  | m, n, 0 => [n-'0=n] (m -' n)
  | m, n, p => {?}

It is defined by pattern matching, so each clause has its own type. For example, the type of the first clause is m -' n -' 0 = m -' n. You cannot see that type when you read the code, and it could be a non trivial task to calculate it in your head. But knowing the type helps to understand why the proof on the right side of => looks the way it does. It would be nice if IDE could show me the type explicitly.

One way to do that is to use inlay type hints. An example in Kotlin:

Here : List<Path!> is a hint that shows a type of the foo variable that is not specified explicitly. In Arend that might look like this:

\func -'+assoc (m n p : Nat): m -' n -' p = m -' (n + p)
  | m, n, 0 => [n-'0=n] (m -' n) : m -' n -' 0 = m -' n
  | m, n, p => {?}

[ice1000]

Currently you can select an Arend expression and do Ctrl Shift P to show its type

[marat-rkh]

Yeah, I use it. I believe type hints might be more convenient when you mostly read code. Selecting and invoking the action for each clause is too tedious.

[ice1000]

FWIW the 'show type' action is kinda expensive

[marat-rkh]

Oh, I see. That could be a problem, indeed.