bug#38485: Customizing glyph widths

[Eli Zaretskii]

> Cc: casouri@gmail.com, 38485@debbugs.gnu.org
> From: Clément Pit-Claudel <cpitclaudel@gmail.com>
> Date: Thu, 5 Dec 2019 09:26:12 -0500
> 
> > Are you saying that we _can_ not widen them, or are you saying that we
> > _must_not_ widen them?  If the latter, can you explain why not?
> 
> That we must not.  I set up these prettifications specifically to make the 
> characters narrower and reduce visual clutter; widening them would defeat 
> that purpose.

So in this case the alignment considerations are thrown out the
window?

> I commonly write things like this:
> 
>   Lemma lcomm: forall x y, x ~+~ y <-> y ~+~ x.
>   Proof. induction x; cbn; try rewrite IHx; reflexivity. Defined.
> 
> with prettification, it looks like this:
> 
>   Lemma lcomm: ∀ x y, x ⨤ y ↔ y ⨤ x.
>   ∵. induction x; cbn; try rewrite IHx; reflexivity. □.
> 
> What I really want is this:
> 
>   Lemma lcomm: ∀ x y, x  ⨤  y  ↔  y  ⨤  x.
>   ∵. induction x; cbn; try rewrite IHx; reflexivity. □.
> 
> but not this:
> 
>   Lemma lcomm: ∀      x y, x  ⨤  y  ↔  y  ⨤  x.
>   ∵    . induction x; cbn; try rewrite IHx; reflexivity. □      .

Why is "Proof" treated differently from the other symbols?  How would
the user know which one is which?