fully recursive NL/Formula grammar
We need to be able to handle cases like
Let $S = \{ n \in Z | \text{$n$ is even} \}$where NL contains a formula that contains NL, which contains a formula again.
I guess we need have parallel categories in the NL and F subgrammars, and wherever category NX is allowed also a category FX is allowed.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information