New inspection: redundant explicit argument

[marat-rkh]

Consider the following code:

\func foldr-append {A B : \Type} (** : A -> B -> B) (e : B) (xs ys : List A)
  : foldr ** e (xs ++ ys) = foldr ** (foldr ** e ys) xs \elim xs
  | [] => idp
  | :: x xs => pmap (x `**`) (foldr-append ** e xs ys)

Here, recursive call foldr-append ** e xs ys can be rewritten to foldr-append _ _ _ _. We could have an inspection that detects such cases and suggests a replacement.

I am not sure if it is cheap enough to run such inspection on the fly, so it could be

• disabled by default
• executed only before commit
• a separate action that you run explicitly