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

Re: [tlaplus] Re: "Uknown Operator" in refinement mapping

Hillel's example does not show a bug in anything but the spec.  Look 
below to see why.


-------------------------------- MODULE main --------------------------------

Abstract == INSTANCE abstract

Refinement == abstract!Spec


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/379f3349-7b39-4067-9065-a84409a63aaa%40googlegroups.com.