Feat: Add a Html-highlighted version of #check (grayed-out implicit arguments)

[mirefek]

#checkh name shows the signature of name with dimmed implicit arguments,
#checkh' name also includes them in the String export.
Zulip discussion:
#general > Dimming implicit arguments in `#check`

[mirefek]

[Vtec234]

Hi! I think this command may be a better fit for mathlib. ProofWidgets focuses on general and reusable abstractions for building user interfaces (in particular components that involve TypeScript code so that mathlib can avoid a dependency on NPM), whereas this is more of a specific usecase.

[mirefek]

To be honest, I was not really sure where this should belong. I thought it was low-level enough that a potential user might not want Mathlib dependency. Batteries would feel like a natural option if it didn't require ProofWidgets...
So you would recommend somewhere in Mathlib/Tactics ?

[Vtec234]

I agree there is no great place to put this. It only relies on the JSX syntax and HtmlDisplay, so maybe these should eventually be migrated upstream; but in the meantime let's just merge it after all.

Batteries would feel like a natural option if it didn't require ProofWidgets...

Maybe you mean 'did require'?