XSemantics syntax is too strict

[SimonCockx]

For example, I can't have an empty auxiliary { } statement. These kind of checks seem unnecessary and are a bit annoying when setting things up for a new type system. See also #150 (e.g., the order of auxiliary definitions, rules and checkrules shouldn't really matter)

[LorenzoBettini]

Hi, I'm not sure I understand what's the problem with this specific error: when you start writing auxiliary { } you'll get an error, but as soon you add one the error goes away... or am I missing something?

[SimonCockx]

This is only a small annoyance. I'm getting used to the whole XSemantics setup, i.e., first specifying auxiliary functions, then the judgements. In the first iteration of implementation, I might not need any auxiliary functions though, but I prefer to already specify an empty auxiliary { } statement. I don't see a reason why it should be disallowed, hence this issue. Again, this is only a small annoyance though.

Thank you for following up on all my issues btw, your help is much appreciated.