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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 8 Dec 2020 08:44:42 +0100*References*: <cac57bb6-3d36-433e-a1f9-b3747211fe56n@googlegroups.com> <DCC08488-5FEC-4E15-A19C-C1749E2B3F53@gmail.com> <55e16139-6401-44d1-9b21-e4c1e3d694e2n@googlegroups.com> <AAF60449-8329-4E99-B186-9053CF1908B0@TimLeonard.us> <cd36eaeb-0e53-40cf-a5c5-0fd5895d3793n@googlegroups.com>

Perhaps it would make sense to add an operator such as PartialFunctions(A,B) == UNION {[X ->B] : X \in SUBSET A} to the CommunityModules, representing functions from some subset of A to B? Stephan P.S.: Apologies for the typo (missing function brackets) in my reply to the original question. -s
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/BBF48CDE-9CEF-4A42-AB93-908EEEF0EC00%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Initial state doesn't satisfy type invariant***From:*Srikumar Subramanian

**References**:**[tlaplus] Initial state doesn't satisfy type invariant***From:*Tim Leonard

**Re: [tlaplus] Initial state doesn't satisfy type invariant***From:*Stephan Merz

**Re: [tlaplus] Initial state doesn't satisfy type invariant***From:*Srikumar Subramanian

**Re: [tlaplus] Initial state doesn't satisfy type invariant***From:*Tim Leonard

**Re: [tlaplus] Initial state doesn't satisfy type invariant***From:*Srikumar Subramanian

- Prev by Date:
**Re: [tlaplus] A temporal formula to specify that the value of a record does not change** - Next by Date:
**Re: [tlaplus] Initial state doesn't satisfy type invariant** - Previous by thread:
**Re: [tlaplus] Initial state doesn't satisfy type invariant** - Next by thread:
**Re: [tlaplus] Initial state doesn't satisfy type invariant** - Index(es):