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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 7 Jun 2021 16:33:57 +0200*Ironport-hdrordr*: A9a23:Dq4Vca3nzUqRj+BqtGSDzQqjBexyeYIsimQD101hICG9Lfb15ruTdaUguG6NtN9OYhtQ4OxoWZPwMU80kKQbj7X5Uo3SKTUO1FHYXb2KqLGStQEJ9UXFh6tgPYkJSdk9NDSyNyk1sS7CiDPIUOrIueP3tJxBMIzlvjhQpH9RGuhdBnZCe3Wm+xZNNUV77PMCffL2l6033UvdCAoqg9yAdwQ4tqr41qn2ffTdEFM77jEciDVm5gnYmoISfSLoqSv3klt0sNMfGKv+4m/ED2eY0s1SenTnpi/uBlht6bncI6N4dYSxYsV/EESntu5ZD74REIFqdQpFxZDImSkXueiJmQ4pO4BY6n/afG255Tvrnyf61io2gkWSiGOlvQ==*References*: <f71490a1-015b-c6f0-a24f-efe11a7757e4@gmail.com> <CAFteovLeYPyyqzgyBFdZNTBJKRmL2_Am82H7jitLe52yYiKF2w@mail.gmail.com>

TLAPS relies on type information for optimizing the encoding for back-end reasoners, and a typing invariant such as /\ x \in Nat /\ y \in {"foo", "bar"} /\ z \in [ Client -> Int ] is easier to handle than state \in [ x : Nat, y : {"foo", "bar"}, z : [Client -> Int] ] Stephan
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/E0DB055F-55BF-42C3-96C3-C3E0E0B8A022%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] How do you do functions of structures?***From:*Aaron Elligsen

**References**:**[tlaplus] How do you do functions of structures?***From:*Hillel Wayne

**Re: [tlaplus] How do you do functions of structures?***From:*Karolis Petrauskas

- Prev by Date:
**[tlaplus] Re: How do you do functions of structures?** - Next by Date:
**Re: [tlaplus] How do you do functions of structures?** - Previous by thread:
**Re: [tlaplus] How do you do functions of structures?** - Next by thread:
**Re: [tlaplus] How do you do functions of structures?** - Index(es):