Skip to Content.
Sympa Menu

coq-club - [Coq-Club] A question on format strings

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A question on format strings


Chronological Thread 
  • From: Christian Doczkal <christian.doczkal AT ens-lyon.fr>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] A question on format strings
  • Date: Tue, 3 Sep 2019 12:50:47 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=christian.doczkal AT ens-lyon.fr; spf=Pass smtp.mailfrom=christian.doczkal AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
  • Autocrypt: addr=christian.doczkal AT ens-lyon.fr; prefer-encrypt=mutual; keydata= mQINBFIuNbYBEADAiZlQsnkRrXHOkaZ2mZIVNxzcBha3+HhZ8IhtxF4t5QXRNWFLtdwBuE8u D0GMB/Lacm/LujwcI756cPM/7PhrUFAyn1IrYHYsK4/O5gBEgbSBRjD0X8mJ0V3oIm/PtjMC YiXBJwzOMNXOeWp+HcyCR0eh2sQD94gbF9SUOKDoamNB3DbLEHKjYPJ9O3zQw/Xai624OXB0 Wk5yIW77I1mGWhwbWxeHOJ/NmhHEU38YfbxXSzCLeMv98bNTej4oA+cPtMZ94AZOSy/oroMh rsr6wA9PL7NS+B1kRbgv6a5KL9latAI7zPeXcVsYw076rL850PLez/SXDuIr9mud4v8Zvcp9 65vTK4lTAD4C4vneNRGt4iwCOIgGsAN6BgqEgr7EwLX8dAX57OXPKZj0/0TdCbu+qsoSrQ3u +Ul6k374jFeIndqg/e9NiJbHjYAuug3cZZ6mH24SXWtTd4hGWi6f26tQQcRyGiduZkw5Wn26 g0UVgps7o2zHwlp9LJVjL3pCw7a9tKOfZaH+h7dV5JsA/Oq+7F3PhTbyNagi4A9igw+0qU+n Ws/nZDVMRiUv+1HY4PG8q6iEGSfHHjwW8InYS+Ah3stTddJ0sLc+0AGutx8ueTE2Ks14c4c8 aNW5y9bNFI/6/UQmOOwGmBeYC/kjZhjhsC3dTJ9uX4pXlMhpLQARAQABtDFDaHJpc3RpYW4g RG9jemthbCA8Y2hyaXN0aWFuLmRvY3prYWxAZW5zLWx5b24uZnI+iQJUBBMBCAA+AhsDBQsJ CAcCBhUKCQgLAgQWAgMBAh4BAheAFiEE6jiiZvHNwp19meaCj7B3SJxkuY0FAluX/3QFCQtK /T4ACgkQj7B3SJxkuY24UQ/+L9DFIx/Z8+SGhA6h8+JvfM/N3l2IT9fsDfPTLVLoyYk6j0CR T/DTGOzmh9fCCcYJbxeNeR63vwo13B0nCKfJE1sudpJCqM/6xMMeq4IcQo4Sump24iP3V9Dg iicyXowcaMTAonwadhRyGoykdXWkaHTLLbFtuF10oO0geoyM0gy/quVmONvDZVDX6WRk0DHN vx/fRCnr3pHFm1TDp5XatQbxwDH7MqX7zS5P9onkro3lqIJiekXyPeeUVZn1OWI4Ai8RgUTZ w5RNgoj/iPtCdu0yVrL5EwEikSRrrPwqp/VLNw+hslgrdI9rtv6bf2x4AshjBoi/S4MUt3s5 3hTiLhkxMeD6iPFv70SKYdYqkhN1Y7owb0L4u9/gdODvCOofo97mv0UCTvY0hpDpiyYDM/tr 6fwSVGObSYLmjzVjrwWB1gQaDsn+ghSwwGutGEHSPdwHIy4e5qCYDaUPRWSdfxfGx3ZOO9f4 s28ufT9tJbvZK2/DPpxhGEcVQE+vMoopWJma8NoZW4IbQzqg/8vFd4w9MsMDqDsbhgOlKtpv 3GEixafUMF5wJDHEpYQaWKWf1lLg7u8FIefCaJC9E/0Wl7XhmhYx0wPQ71fOhEGmf7P1DUdy OTrZtS+O3RcM54zQjlK9lweIOPYpwW8BvgNI4+E/ev1Fv31duTniNbxSeku5Ag0EUi41tgEQ ALKCkrZVjm7Jr6wZkeYMPs+OCtICbILfcRODKsM/JxEdcxbr99UA5GGi94OXGxvkQf5yLQxG hCzrLJVbrpBvl+stg72/8DrYGCCSl72gxLTTInfFxEvH3xGpBP/oMXdGjk+jxWA48opzsaar Bd9PxvFNZoWjB9jdgzBPpNMa/ykw4ATVC2fzC5xuo4fwUsl1Wu8DFLbMVwSHGXCqmV6QYUXf 0i3EKnNkKRH3a3rd7JsrC0/6lBL8sLoT54K3J6NGii6dzalhOycsSI4R8czclof3RIy5Mh/Z /rqv4d0OgY2b7QOYnGrITVtyC5UqzGMZx0dnQr5Bm7YOHaCML/LjMoYj2ovFh2zjaU6I/smx 3stVkMRpmqB7/cYPktkpGV8K9S0l6Cgiepn9pymU0/NCBFKXrPuoorKz0+X6j6YsSy7PJ1KC EIh2nSPdhB7/4ezw3DB/COfTE8EY+xbPpTF4DfI+4ARrbP953C4Z2JC7xHUGqH+D/TQ2qYiT mfHdZTrzvWYHCERApZKq1Erdpl7mHfFnwyoDB8OqS9QWfwz3Ql8TeoFPP5LdS4PHkEqog2vH j6njJnLDLUcU5OGKVrGiu8qdMGyIJNeyY6eGcl+4RR+iNJaCVSwLDB+otbxCg2cemGAfvTI4 GGpwxXuf8/r8JL9l9Jgr/zw2WroiZwOJDhPpABEBAAGJAiUEGAECAA8CGwwFAlm49m4FCQlr 9DgACgkQj7B3SJxkuY0LJQ//cnR3s/JabXBWAbkjHbHkISOGg9QA0atjtWcYTR6wHt9keERf CCEe6hEz0JjwDAmOnEMH3ehunLYiENAS3HSw5jbh7qS4EiJt1zDEpe7P8lDmuk+nGwYyI7dA kJMU7SSBys3ZDbkz5ejGocGvfq1tW/dB/0o5OVT8h9STM/Gwka1YZdNdKJtA+WGN5NSfEVQ6 CDePi6qWWBc2DYPy5XAK3HD4UpxmX6nBlDRoW1L04sAY6+NlpusxsAK3bbI8aElunVYtEL6k cJyAvVt/VXC4GbmrPduAJ8+799qk6uwbr42EJO12+S9qb5njH4+rVdngPWyiQpugGwMOR4A2 KFB/V/oFi8Ai/ep2tatXilwiXPnewu+RDY5+rqhbwVuf1mQO0owBUe5ZxraMndEBFQIqyFo9 vM6UJ/4XAo7NqEoMgFuM/oA51vJFQGcc++Nl9UVaO7ss101K6pJGIueaYRI+iZ2fbyrxWhRx hqYkpyxvIHdgUDP9h9VY3rYAOfSiMXAcYDGx1ztR36ARt+ZzygOI/55yf6CT04WtSDUQ6z3w 5UkqbX/YPLYjbzMkZAEfZBBy+PNaW2N779aiqWLfDHe47mt3L8B3/Tkh5vfAG7Rch4NmlXFI Idls4nQdC5B213rkODbQOvFU0BKljxbWmCJoEhprrRBUTui6L9zaF49OWrKJAjwEGAECACYC GwwWIQTqOKJm8c3CnX2Z5oKPsHdInGS5jQUCW5f/dAUJC0r9PgAKCRCPsHdInGS5jbhiEACn BN29HGmlJLqLyh3H/lbZDKXWQg1KzlTiMcL/EUwrUhYLK0Lm9tsHNggQfqtnAJTW+0g/Q9wG sLDAyTaHtgPUym8jFWtPv45YfHElSwdUSzy80ZKxcw5WsD4ofpvKite4j7ehzegJF0nJ1JlP FGwRDaRoVig+cQDqjtK3fCOflsTgIcqt4gB/44x79zWSfdqag64RLMmthVWq+eRCQzFNaOH6 nSUcpmXe/OTMRYx3weqsmtLAm4kcHRdGR6bmlmOcng5gleT2TImwiW3KbRzDGFIzj/gcx6Xv sonEdKGv/VgUWYvqxSnktd9/YWVUQaj+XN+C7S2p8VThkwzTxbG30jU8rgjCgci3dObipm5w kvXdI2Ojrk5wz2yDtQS1DHjE4GeC0fP2XinC3IeH8uXl1ggCxH7emzETZgM+hiM1Ijt4M80n hjbMB989q8CheOhlT/6R0G7BWKAoFo/nx+KqzWNoRX2tWPaNrbxiPdTwe3l6imJ0LYqMoNGG 52+WCE98JsihXE5x62m2vEFztbJ/CyyyIAgcdQdnVeh9N2Bhx99LdKWmxb1DLGi4nsBdtlOr 4nGHbO36PbBvPp0UhMGMe8UQs41NBGp2u4avbPdQYcMBdURHHgcVPMUTQIN7D1zGPNKw/31f 11BY4o3BdbLXAggJ3dGbm2ZAnj3OQRK3Sg==
  • Ironport-phdr: 9a23:/mvLlhfJxs56Y/OgKOZaI36plGMj4u6mDksu8pMizoh2WeGdxcu9YB7h7PlgxGXEQZ/co6odzbaP6ea5BjdIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfK1+IA+roQjTuMQdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LptRRT1iikIKiQ5/XnJhMJwkaxVoxyvqBJwzIHIe4yVO+Zyc7nac98GS2dMXMBcXDFBDIOmaIsPCvIMMPhYr4nnplsOtge+BQi2C+Pp1zRGiHj20rE70uQiCw7G2BErEtUSv3TUttX1NbwSUfy0zKbSyzXPde5Z2TDh54nJcRAuu/WMUKlufsrX0kkjDgfFj1WXqYzjJT+V2P4NvnGd4uF9Vuyvk3Yqpxx+rzSz3MshiIvEipgIxl3F9yh12pg5KcOmREJjfNKpH4dcuzuYOoZ0WM8uXm9ltDwnxrEapJK2ejUBxo49yB7FcfOHdpCF4hL9W+aVJjd1nHZld6ikiBmp70es0PPzVs+v0FpTqipEkt7MtnYX2xzd8MiLUvp9/kG/1jaTzw3f9+5JLVwumafZKZMt2KM8m5sRvEjZACP6hlv6gLeTdko+++io7+rnYq/hpp+ZL4J7lgH+Mr4vmsykHeQ4MxIBX26B9euh073s4Uz4QLZQgf0yiaTWrpbaJd8Cqq69Aw5V1YAj5wyxDze8yNgYh2UILEpZeBKbiIjkI03BIPfhDfumn1uslCpryOvdM736ApTNK2DDn637cbZ87U5c0gszwspF65JaELFSaM70D0T2rZnTCgIzGw2y2efuTttnha0EXmfaKa+DMbjOsFaOrs4oKPuPbYtd7D39Mfk++//nizk1nlQPfqCt9ZYRczW8D/NgZUuDNym/yuwdGHsH61JtBNfhj0ePBGYKNiSCGpkk7zR+M7qISILKR4SjmruEhXzpE5tNI2RXDVbKH226LtzYCcdJUzqbJ4paqhJBTaKoEtRz2Be18QvrzLwhIPCGonRF56Km78B84qjorT939TFwCJ3MgWWERWt52G4OXHoyzad550JnmA+O
  • Openpgp: preference=signencrypt

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

Attachment: signature.asc
Description: OpenPGP digital signature



  • [Coq-Club] A question on format strings, Christian Doczkal, 09/03/2019

Archive powered by MHonArc 2.6.18.

Top of Page