[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: TLC reports error (undefined identifier), but it's defined...

From: Leslie Lamport <tlaplus.ll@xxxxxxxxx>
Date: Sat, 1 Feb 2020 17:35:36 -0800 (PST)
References: <877e9t2z45.fsf@tpad-m.i-did-not-set--mail-host-address--so-tickle-me> <8312fbba-ed17-456e-9f11-51141643d4e2@googlegroups.com>

Please look up CHOOSE and see what

CHOOSE u \in Users : ...

means. Then look up \E and see what

\E u \in Users : ...

means.

--
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/700e0276-0a7d-44dc-9050-f3596eed2ab2%40googlegroups.com.

Follow-Ups:
- [tlaplus] Re: TLC reports error (undefined identifier), but it's defined...
  - From: Johan Persson

References:
- [tlaplus] TLC reports error (undefined identifier), but it's defined...
  - From: 'Marko Schuetz-Schmuck' via tlaplus
- [tlaplus] Re: TLC reports error (undefined identifier), but it's defined...
  - From: Johan Persson

Prev by Date: [tlaplus] Re: TLC reports error (undefined identifier), but it's defined...
Next by Date: [tlaplus] Re: TLC reports error (undefined identifier), but it's defined...
Previous by thread: [tlaplus] Re: TLC reports error (undefined identifier), but it's defined...
Next by thread: [tlaplus] Re: TLC reports error (undefined identifier), but it's defined...
Index(es):
- Date
- Thread