New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: a non-terminal simp linter #11246
base: master
Are you sure you want to change the base?
Conversation
This PR accompanies #11246, squeezing some non-terminal `simp`s highlighted by the linter until I decided to stop!
The squeezing continues! All found by the linter at #11246.
950732f
to
de6d27f
Compare
de6d27f
to
71263f3
Compare
This PR accompanies #11246, squeezing some non-terminal `simp`s highlighted by the linter until I decided to stop!
The squeezing continues! All found by the linter at #11246.
This is great! Is it possible to add a whitelist for some following tactics, for instance it has been agreed on zulip in the past that some patterns like |
This PR accompanies #11246, squeezing some non-terminal `simp`s highlighted by the linter until I decided to stop!
The squeezing continues! All found by the linter at #11246.
This PR accompanies #11246, squeezing some non-terminal `simp`s highlighted by the linter until I decided to stop!
The squeezing continues! All found by the linter at #11246.
This PR accompanies #11246, squeezing some non-terminal `simp`s highlighted by the linter until I decided to stop!
The squeezing continues! All found by the linter at #11246.
This PR accompanies #11246, squeezing some non-terminal `simp`s highlighted by the linter until I decided to stop!
The squeezing continues! All found by the linter at #11246.
This PR accompanies #11246, squeezing some non-terminal `simp`s highlighted by the linter until I decided to stop!
The squeezing continues! All found by the linter at #11246.
An implementation of a syntax+
InfoTree
s linter checking for non-terminalsimp
s.The linter equates "non-terminal" with "does not strictly decrease the number of goals".
Accompanying PRs squeezing a few of the
simp
s flagged by the linter:squeeze_simp
s arising from linter #11259Zulip threads: