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