[Meta.synthInstance] ❌︎ CoeT Type Nat Prop ▼
[] new goal CoeT Type Nat Prop ▶
[] ❌︎ apply @instCoeT to CoeT Type Nat Prop ▶
[] ✅︎ apply @instCoeTOfCoeDep to CoeT Type Nat Prop ▶
[] ✅︎ apply @instCoeTOfCoeHTCT to CoeT Type Nat Prop ▶
[] ❌︎ apply @instCoeHTCT to CoeHTCT Type Prop ▶
[] ✅︎ apply @instCoeHTCTOfCoeHTC to CoeHTCT Type Prop ▶
[] ❌︎ apply @instCoeHTC to CoeHTC Type Prop ▶
[] ✅︎ apply @instCoeHTCOfCoeOTC to CoeHTC Type Prop
instead of
[Meta.synthInstance] ❌️ CoeT Type Nat Prop ▼
[] new goal CoeT Type Nat Prop ▶
[] ❌️ apply @instCoeT to CoeT Type Nat Prop ▶
[] ✅️ apply @instCoeTOfCoeDep to CoeT Type Nat Prop ▶
[] ✅️ apply @instCoeTOfCoeHTCT to CoeT Type Nat Prop ▶
[] ❌️ apply @instCoeHTCT to CoeHTCT Type Prop ▶
[] ✅️ apply @instCoeHTCTOfCoeHTC to CoeHTCT Type Prop ▶
[] ❌️ apply @instCoeHTC to CoeHTC Type Prop ▶
[] ✅️ apply @instCoeHTCOfCoeOTC to CoeHTC Type Prop
Further, using the wrong font, one might see inst✝️ instead of inst✝︎, which is distracting.
Beneficiaries
Better support for custom fonts helps in particular the international community as for example Chinese, Japanese or Cyrillic script might require usage of a custom font. E.g. JuliaMono is defacto a solid choice and also used by live.lean-lang.org.
Maintainability
There is some potential issue to consider about unicode characters that look identical.
Community Feedback
There was some private feedback by Joachim Breitner (@nomeata) that ❌︎ and ✅︎ in the trace output is not nice as they are harder to recognise.
Zulip discussion suggests this could be a valid approach if it doesn't create new pitfalls for the user.
Impact
Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.
Proposal
Occasionally, Lean uses emojis, for example it uses
✅❌💥
for debugging. The proposal is to use the variant selector with\uFE0F
followed:In particular, use
(which look the same, but are different to the currently used
✅❌💥✝▼▶
)User Experience
Minor improvement, but helps with using custom fonts. See for example live.lean-lang.org:
which displays
instead of
Further, using the wrong font, one might see
inst✝️
instead ofinst✝︎
, which is distracting.Beneficiaries
Better support for custom fonts helps in particular the international community as for example Chinese, Japanese or Cyrillic script might require usage of a custom font. E.g. JuliaMono is defacto a solid choice and also used by live.lean-lang.org.
Maintainability
There is some potential issue to consider about unicode characters that look identical.
Community Feedback
There was some private feedback by Joachim Breitner (@nomeata) that
❌︎
and✅︎
in the trace output is not nice as they are harder to recognise.Zulip discussion suggests this could be a valid approach if it doesn't create new pitfalls for the user.
Impact
Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.