feat: allow short config syntax (+opt / -opt) for several parsers

[Rob23oba]

This PR changes the parsers of #reduce, the ext attribute, and match to allow the use of the +opt and -opt syntax for configuration in a similar way to how they are handled in let. Additionally, #reduce and the ext attribute can now receive both options in any order (e.g. @[ext -iff -flat], @[ext -flat -iff], @[ext -iff -flat +iff]).
Examples of new syntax:

#reduce +types +proofs xyz
@[ext -flat -iff]
match -generalizing xyz ...

[nomeata]

Thanks for trying to help. Im a bit worried about the form of contributions, though. Probably the behavior is desirable, but thats unfortunately not the only question here. Even if it's clear that it goes in the right direction (although even that requires someone to sit down and context switch and think it through), the code needs careful review, and for every piece of code (even if correct, useful and well-written) that's added there is ongoing maintenance cost, which is higher if the code wasn't written by whoever has to do the maintenance.

So even if reviewing a PR would be less effort for the maintainer than doing it themselves (which is not even always the case), there is a significant effort involved with reviewing and accepting PR. That effort is often spent better on some of the other myriad of missing features and issues.

Submitting an unsolicited PR (and expecting it not to be ignored) only makes sense if that PRs happens to fix something that's more useful than whatever the maintainer could have done otherwise with the time they would spend on reviewing and ongoing maintenance.

I know that this is frustrating and unsatisfying for an external contributor willing to help with Lean. But it's unavoidable while we need to maintain focus while pushing Lean forward in this phase of the project.

TL;DR: Unsolicited PRs may just sit there, sorry.

(If this was created after a discussion and encouragement from a team member it would be a different story, but I didn't see a mention here.)

[Rob23oba]

Yeah, you're right; after submitting the PR I also realized that I should've at least made an RFC and had some discussion before instead of RFC. Otherwise, there are always maintainability concerns and review times spent by FRO members that introduce friction for going forward. I'm curious though; what are the current plans moving forward? (I guess the module system comes to mind but I assume there's more planned?)

[nomeata]

Good question actually, looks like the next roadmap update isn't out yet. Should happen soon, but I don't know the roadmap roadmap :-)