[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#38485: Customizing glyph widths
From: |
Clément Pit-Claudel |
Subject: |
bug#38485: Customizing glyph widths |
Date: |
Thu, 5 Dec 2019 09:26:12 -0500 |
User-agent: |
Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.2.1 |
On 2019-12-04 22:34, Eli Zaretskii wrote:
>> Cc: casouri@gmail.com, 38485@debbugs.gnu.org
>> From: Clément Pit-Claudel <cpitclaudel@gmail.com>
>> Date: Wed, 4 Dec 2019 15:53:43 -0500
>>
>>> No, it will simply make each prettified symbol take up the same width
>>> as the original characters of the symbol that were composed. Isn't
>>> that what everyone would want, and want for _all_ prettified symbols?
>>
>> Probably not. In proof-general, we display 'forall' as ∀ and 'exists' as ∃.
>> In my own configuration I also change "Qed" to ■ "Defined" to □, and
>> "Admitted" to 😱. These shouldn't be widened, I think — especially not the
>> last ones (there is a case to be made for widening forall, since otherwise
>> we might get indentation issues, but in Coq Qed, Defined and Admitted don't
>> introduce indentation changes, so it's safe not to widen them.
>
> 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.
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. □ .
Clément.
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/03
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/04
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/04
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/04
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/04
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/04
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/04
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/04
- bug#38485: Customizing glyph widths,
Clément Pit-Claudel <=
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/05
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/05
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/05
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/05
- bug#38485: "prettified" symbols, Richard Stallman, 2019/12/05
- bug#38485: "prettified" symbols, Eli Zaretskii, 2019/12/06
- bug#38485: "prettified" symbols, Richard Stallman, 2019/12/06
- bug#38485: "prettified" symbols, Clément Pit-Claudel, 2019/12/06
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/04
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/04