The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi Christian,

Interesting question!  I've played quite a bit with the printing boxes to make
Hoare triples print nicely, but I think what you want is outside of their
current scope... you basically want indentation "for the first line only", or
*negative* indentation for the second line.

I would not know of a way to do that with the tools provided currently, but
maybe the underlying OCaml formatting machinery has a way? I am not familiar
with that, unfortunately.  Might be worth submitting a feature request on GH?

; Ralf

On 03.09.19 12:50, Christian Doczkal wrote:
> Hi,
> 
> I have been toying around with format strings and I am wondering if it is 
> possible to craft a notation exhibiting the following behavior for some 
> relation symbol (e.g., ≡ )
> 
> - short expressions are printed on one line: u ≡ v
> - if the whole expression does not fit on a single line, it is indented as 
> follows:
> 
>   <some long expression>
> ≡ <another long expression>
> 
> That is, I would like to have the relation symbol at the start of the 
> second line and indent the first line such that both long expressions start 
> on the same column. 
> 
> Thanks in advance.
> 
> Best,
> Christian
> 

-- 
Website: https://people.mpi-sws.org/~jung/