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: Dec 20 2023 at 11:08 UTC