The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hi Gabriel,

Indeed, it's a cool trick; I wonder if something similar could exist for 
cases like

[ H: False         |- _ ] => congruence
[ H: True /\ False |- _ ] => destruct H

being rendered as

[ H: ⊥         ⊢ _ ] ⇒ congruence
[ H: ⊤ ∧ ⊥ ⊢ _ ] ⇒ destruct H

Clément.

On 03/11/2016 10:27 AM, Gabriel Scherer wrote:
> Since this thread in in the outside-the-box-thinking category, people
> may be interested by Elastic Tabstops that solve this indentation
> problem:
>   http://nickgravgaard.com/elastic-tabstops/
> 
> On Fri, Mar 11, 2016 at 10:22 AM, Pierre Courtieu
> <pierre.courtieu AT gmail.com>
>  wrote:
>> Hi,
>>
>> Concerning prettification there is one problem that is difficult to solve:
>> indentation. Look for example at the following code that is indented for
>> non-prettified display:
>>
>> forall x y, x +
>>             y.
>>
>> This will not look good if prettified:
>>
>> ∀ x y, x +
>>             y.
>>
>> And conversely a good indentation in prettified mode would not look good in
>> non prettified.
>>
>> In pg+company-coq indentation is done according to the current mode
>> (prettified or not), but user opening the file with the other mode will 
>> have
>> ugly indentation.
>>
>> P.
>

Attachment: signature.asc
Description: OpenPGP digital signature