[tlaplus] Minimum level bound on an operator?

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

I'm currently working on developing a semantic error test corpus, which is basically a large set of tiny TLA+ files that trigger all the semantic errors in SANY. This is an amusing sort of reverse-engineering process where I look at the code where an error is being raised and try to guess a TLA+ parse input that will trigger that error. There are a few I'm puzzled by: in particular, this one seems to imply it's possible for operators to have a lower bound on their accepted levels?

"Level error in applying operator " + opDef.getName() + ":\n"

"The permitted level of argument " + (j+1) + " of the operator argument "

+ (i+1) + " \nmust be at least " + opDef.getMinMaxLevel(i, j) + ".");

Does anybody know of an operator with a level lower bound, or is this dead code from a previous incarnation of the level-checker? Thanks!

Andrew Helwer

-- 
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 visit https://groups.google.com/d/msgid/tlaplus/5dab69b1-17ab-44dd-9b28-9ba58a8de00fn%40googlegroups.com.