Zulip Chat Archive
Stream: metaprogramming / tactics
Topic: register private name
Huajian Xin (Oct 16 2022 at 03:52):
Is there any method to register private name? I tried to run tactic if form of exact match ... with | ... | ... and got the error message failed to register private name '_match', , prefix has not been registered. Is there any way to figure out that?
Alex J. Best (Nov 17 2022 at 21:38):
Can you give a full #mwe of what you are trying to do?
Last updated: May 02 2025 at 03:31 UTC