Improved type rendering

[nomeata]

The current way Loogle renders types can become very verbose. What would be a better way?

• Certainly [C t] instead of [inst : C t] would be good if that name isn’t mentioned.

• How about Nat instead of (n : Nat)? if n isn’t mentioned?

  But names can be very useful find : (needle hey : String)…

• simply R instead of (R : Type u_2)? Again maybe only if the u_2 is not mentioned anywhere else?

Unfortunately, the signature syntax before : doesn’t allow unnamed arguments (Nat), and the syntax after : doesn’t allow binders without types (R).

Also, should #check use the same syntax? The documentation generator?

Ideally, the code that does all this is not loogle-specific and lives in Lean or Std.

[Shreyas4991]

I think the first change is definitely welcome. For the second one, the closer it is to the way we write defs, the easier it might be. Just to get it on record for this issue: Removing implicit arguments would be nice.

Overall, whatever changes are made, I propose that at least in the backend at the API level, each hit could have multiple variants of type signatures. On the front end, some safe default can be used and we can provide users options on how they wish to see the type signatures.