Skip to content
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

new modifier # for symbol elimination. #24

Open
kohlhase opened this issue Oct 25, 2024 · 1 comment
Open

new modifier # for symbol elimination. #24

kohlhase opened this issue Oct 25, 2024 · 1 comment
Assignees

Comments

@kohlhase
Copy link
Collaborator

kohlhase commented Oct 25, 2024

When I am annotating something, I often come into the following situation:
Screenshot 2024-10-25 at 08 41 55
I have an annotation I want to make but I realize that the two choices are morally the same symbol, and (in this case) 0 should import 1. In this case, I would like to type 01# to be placed in an editor of my choice (probably via the $EDITIOR environment variable) with both of the files loaded so that I can remedy the situation before I go on annotating. In this case I would import the mv module from smglom/mv in mathtalk.en.tex and remove the \symdecl*{iff} there. This is short and painless and gets rid of an otherwise annoying quality issue then and there.

Of course in the example above, there might also be three or more files involved (or choice numbers larger than digits), so we need to generalize the interaction slightly.

This could build on #27, so that should be done first.

@kohlhase
Copy link
Collaborator Author

Ah, I see that this is a bad example above, since it is an artefact of #20, but the situation described above exists nonetheless

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants