Jason Rute (Oct 04 2020 at 01:22):
I’m experimenting with some stuff, and I’d like to know if it is possible to attach arbitrary information (say a list of natural numbers) to the tactic state, so that later tactics can read it. (I see the tactic state has some sort of user data so maybe it is possible with that. It might also be magically possible with meta variables.)
Jason Rute (Oct 04 2020 at 01:26):
Also, I’m doing something hacky here (for proof recording), so (1) I have to use the built in tactic state instead of passing information in the usual tactic way, and (2) this isn’t something that is supposed to be PRed.
Bryan Gin-ge Chen (Oct 04 2020 at 01:38):
This isn't exactly what you're asking for, but there are some examples of custom tactic modes linked in this thread, including some where you can store extra data with the tactic state; in particular, rb_map_ts from the Lean tests seems relevant.
Jason Rute (Oct 04 2020 at 01:48):
Yeah, I trying to avoid that. I want to work with the current tactics (slightly modifying some library code like
istep). I want to see some information about what has been run before in that proof.
Jason Rute (Oct 04 2020 at 01:49):
Actually, I think I can do it with
tactic.set_options. I can store
string associated with names. I think that should work for my use case. (But I still need to test it out.)
Jason Rute (Oct 04 2020 at 02:07):
Yes, that works exactly as I want. (Or at least good enough. I can't directly store a list, but I can make a linked list using names as pointers, or serialize a list into a string.)
Last updated: May 13 2021 at 21:12 UTC