I think you want to writeTHEOREM SOSpec => HashmapSpec!HashmapSpecThe formula SOSpec is defined in the module that introduces the refinement, not in the one for the high-level spec.StephanOn 7 Apr 2020, at 15:00, Åsmund Kløvstad wrote:Hi, thank you for the response. Here is a minimal example using the same hashmap spec and a very minimal SOSpec that gives me the same error.- ÅsmundOn Monday, April 6, 2020 at 11:24:34 PM UTC+2, loki der quaeler wrote:Hi,This sounds potentially like a parsing bug; could you provide a fully contained MODULE file in which this is reproducible?Thanks - lokiOn Monday, April 6, 2020 at 3:57:33 AM UTC-7, Åsmund Kløvstad wrote:Hi,I am working on a refinement mapping and getting an error I do not understand.I'm attempting to show that SOSpec implements the spec hashmap and I've got the following in the module that contains SOspec:(**************************)(*Split-order spec        *)(**************************)SOSpec == SOInit /\ [][SONext]_<>(*********)(*A refinement mapping of the hashmap spec with the map defined by the SOFind action*)(***********)HashmapSpec == INSTANCE hashmap WITH map <- [k \in PossibleKeys |-> SOFind(k)](********************************)(*Split-order implements hashmap*)(********************************) THEOREM SOSpec => HashmapSpec!SOSpecThe toolbox is giving me the error "Unknown Operator: SOSpec" after the bang on the last line. (And the same error if I try to check the property HashmapSpec!SOSpec with TLC)It seems to me like SOSpec is very clearly defined a few lines earlier, so what does this error mean? -- 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/5794ed15-b774-4acd-81c0-b464924fa4cf%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/E22C2A19-C580-4630-9287-DC141E808B63%40gmail.com.