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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 7 Apr 2020 15:09:01 +0200*References*: <5ea69a07-1f03-46fb-8a28-7fa7037dfa17@googlegroups.com> <66188707-0c64-4d23-98d3-ede4f84fe1c7@googlegroups.com> <5794ed15-b774-4acd-81c0-b464924fa4cf@googlegroups.com>

I think you want to write THEOREM SOSpec => HashmapSpec!HashmapSpec The formula SOSpec is defined in the module that introduces the refinement, not in the one for the high-level spec. 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/E22C2A19-C580-4630-9287-DC141E808B63%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Re: "Uknown Operator" in refinement mapping***From:*Åsmund Kløvstad

**References**:**[tlaplus] "Uknown Operator" in refinement mapping***From:*Åsmund Kløvstad

**[tlaplus] Re: "Uknown Operator" in refinement mapping***From:*loki der quaeler

**[tlaplus] Re: "Uknown Operator" in refinement mapping***From:*Åsmund Kløvstad

- Prev by Date:
**[tlaplus] Re: "Uknown Operator" in refinement mapping** - Next by Date:
**Re: [tlaplus] Re: "Uknown Operator" in refinement mapping** - Previous by thread:
**[tlaplus] Re: "Uknown Operator" in refinement mapping** - Next by thread:
**Re: [tlaplus] Re: "Uknown Operator" in refinement mapping** - Index(es):