rfc: unused variable warning should suggest `_` prefix

Stream: lean4

[Alok Singh]

prefixing underscores suppresses the warning. the rfc is that an unused variable warning should suggest this as a fix, but mention that it should be intentional.

Maybe a message like:

unused variable `foo`. If this is intentional, prefix it with an underscore like `_foo`.

would be good. Also, should 'unused' be capitalized?