RE: [tlaplus] Is there any way to typeset the a % b operator as \pmod{b}?

From: "'Leslie Lamport' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>

Date: Thu, 30 Mar 2023 19:41:23 +0000

Accept-language: en-US

Msip_labels: MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_ActionId=00b05b01-2ab5-41ac-b4e2-d04c4b6ab251;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_ContentBits=0;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_Enabled=true;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_Method=Standard;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_Name=Internal;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_SetDate=2023-03-30T19:34:31Z;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_SiteId=72f988bf-86f1-41af-91ab-2d7cd011db47;

References: <c63b3ceb-23be-4f81-825b-e978c6e55123n@googlegroups.com>

Thread-index: AQHZYzzMh7clLYRD7EimixgBCsY4Ia8TttNA

Thread-topic: [tlaplus] Is there any way to typeset the a % b operator as \pmod{b}?

Hi Andrew,

Since I wrote that tool, I presume it’s easy to modify the code to make it do that. Just note that there are probably two places where % is handled, one for when it appears in a TLA+ formula and one for when it appears in prose.

Cheers,

Leslie

From: tlaplus@xxxxxxxxxxxxxxxx <tlaplus@xxxxxxxxxxxxxxxx> On Behalf Of Andrew Helwer
Sent: Thursday, March 30, 2023 12:21
To: tlaplus <tlaplus@xxxxxxxxxxxxxxxx>
Subject: [tlaplus] Is there any way to typeset the a % b operator as \pmod{b}?

Been playing around with the tla2tex.TLA tool. I think it would be cool to have a % b typeset as a \pmod{b}. Is there a built-in way to do this or is editing the raw tex the way to go?

Andrew

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c63b3ceb-23be-4f81-825b-e978c6e55123n%40googlegroups.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/LV2PR21MB32293342A6695D34820190E1B88E9%40LV2PR21MB3229.namprd21.prod.outlook.com.