feat(tactic/interactive_expr): Color instances in the infoview

[YaelDillies]

Change the behavior of the infoview to visually distinguish:

• frozen instances
• typeclass assumptions that are not instances
• unfrozen typeclass assumptions
• non typeclass assumptions

---

The style is very much up for debate! See Zulip. Once we have decided on the style, I will open a preliminary PR to vscode-lean adding the new attributes to the CSS.

[eric-wieser]

Where did the key n.local_uniq_name go?

[eric-wieser]

nit:

Suggested change

	end in h "span" [cn $ var_style ++ " b pr2"] [html.of_name $ expr.local_pp_name n],
	end in h "span" [cn $ var_style ++ " b pr2"] [html.of_name n.local_pp_name],

which is more similar to how it was spelt originally

[eric-wieser]

In the interest of backwards-compatibility with older extension versions, perhaps

Suggested change

	then "goal-hyp"
	else match is with
	| some is' := if n ∈ is'
	then "goal-hyp-inst"
	else "goal-hyp-noninst"
	| none := "goal-hyp-unfrozen"
	then "goal-hyp"
	else match is with
	| some is' := if n ∈ is'
	then "goal-hyp goal-hyp-inst"
	else "goal-hyp goal-hyp-noninst"
	| none := "goal-hyp goal-hyp-unfrozen"

[YaelDillies]

Would it make sense to do

Suggested change

	then "goal-hyp"
	else match is with
	| some is' := if n ∈ is'
	then "goal-hyp-inst"
	else "goal-hyp-noninst"
	| none := "goal-hyp-unfrozen"
	then "goal-hyp"
	else match is with
	| some is' := if n ∈ is'
	then "goal-hyp inst"
	else "goal-hyp noninst"
	| none := "goal-hyp unfrozen"

instead?

[eric-wieser]

No, because inst is a pretty vague CSS class name, as is unfrozen. If in doubt, qualify your names.

[YaelDillies]

Won't the fully qualified name be goal-hyp inst? Disclaimer: I don't understand CSS.

[eric-wieser]

class (which cn sets) is an unordered set of unrelated classnames. You can of course apply styles to things that match both goal-hyp and inst (via the indistinguisable selectors .inst.goal-hyp or .goal-hyp.inst, since conjunction is concatenation), but the danger is that someone else might already be applying a style you don't expect to .inst by itself.

[YaelDillies]

This PR is made irrelevant by the way Lean 4 handles instances. No need to worry about frozen instances anymore.