Thanks for the quick response, Andrew. I've subscribed to that github issue. (I tried to search this GG initially about this but I couldn't find a mention of it. Didn't think to search Github issues).
As an aside, OpenAI Codex was no help whatsoever in diagnosing this issue: it kept insisting that TLC was running against a stale file, and that's why I was seeing an error. And even when I figured out what was causing the problem and asked it to explain why, it gave an incorrect answer!
Me:
The problem was: roots \subseteq Obj
If I do this: roots \in SUBSET Obj
It works. Why?
OpenAI Cdoex:
Given that the same _expression_ works everywhere else in the module, the “roots undefined” at the roots ⊆ Obj line almost certainly means the token on that line wasn’t the same identifier as the one you declared. The most common way that happens is a stray non‑ASCII/whitespace character in the name (e.g., roots spelled with a non‑breaking space or some other invisible character). TLC then sees a brand‑new identifier with no declaration and flags it as undefined. When you retyped the line as roots \in SUBSET Obj, you replaced the bad token with the real roots, so the error went away. If you ever see this again, inspect the line for non‑ASCII/odd spacing (e.g., cat -vet or hexdump -C) and retype it in plain ASCII.
Take care,
Lorin